Simplify/shrink this Lean proof, repeatedly: 24.65% fewer substantive lines; same protected theorem, fresh kernel verification. - offline-ant/wiggums-proof-loop