Why is no one skeptical that the solution is correct? There's not a _single_ comment asking whether this proof is legit or not.
there is a proof in lean4 it's correct by construction
there is a proof in lean4 it's correct by construction