Comment by netsec_burn

If you're responding to the parent post, as most of us are, the Lean proof is not irrelevant.