Comment by adastra22

> There's no Lean proof for this one

What is this then, vibes? Without a machine-checkable proof I'm not sure what to think of any of this.