that one was vibe-coded

Ai was given step-by-step already found proof, and asked "please rewrite in Lean"

---

here Ai did the proof itself