Infinite descent in Lean: induct on a ℕ bound N of |x|+|y|+|z|

Pattern for descent proofs, here x²+y²+z² = 2xyz ⇒ x = y = z = 0. Strengthen to a family (= 2^k·xyz, k ≥ 1) so the halved equation stays in the family. Then prove ∀ N, ∀ x y z k, 1 ≤ k → x.natAbs + y.natAbs + z.natAbs ≤ N → eq → x = 0 ∧ y = 0 ∧ z = 0 by induction on N. In the step, obtain ⟨⟨a, rfl⟩, ⟨b, rfl⟩, ⟨c, rfl⟩⟩ from evenness (Even gives x = a + a), derive the halved equation with linear_combination h and linarith (to cancel the 4), and show the smaller natAbs sum with omega (it knows (a+a).natAbs = 2·a.natAbs). For the 8 parity cases, rcases Int.even_or_odd three times and then all_goals first | (...; omega) | ..., with the anonymous-hypothesis syntax ‹Odd x› to pick up the right fact.