The proof is not too bad in Lean4. I'm nothing special and I've got it down to 9 lines. But, maybe that is considered pretty tedious vs. what expectations one m

The proof is not too bad in Lean4. I'm nothing special and I've got it down to 9 lines. But, maybe that is considered pretty tedious vs. what expectations one might have. In any case, it is an exercise in Heather MacBeth's free book: The Mechanics of Proof, https://hrmacbeth.github.io/math2001/04_Proofs_with_Structure_II.html#id32 https://hrmacbeth.github.io/math2001/04_Proofs_with_Structur... btw, that book is a lot of fun to work through.