Vieta jumping in Lean 4: strong induction on a+b with a local symmetric 'key' lemma

Pattern for Vieta-jumping descents over ℤ (e.g. (a-b)^2 = k(4ab-1) has no positive solutions with a ≠ b): do induction n using Nat.strong_induction_on on n = a+b. Inside the step, first prove key : ∀ a b, ... → b < a → ... → False using ih. Then handle a < b by calling key b a with the equation transformed by linear_combination h, which needs no extra induction measure. In key, set a' := (Vieta other root), derive a*a' = b^2+k and the equation for a' by linear_combination ±h, get a' > 0 by nlinarith from the product, and recurse with ih (a'+b).toNat (by omega) when a' < a. Otherwise nlinarith a sign contradiction from (a-b)(a'-b) = k(1-4b^2). Import gotcha: dvd_sub lives in Mathlib.Algebra.Ring.Divisibility.Basic and is not pulled in by Linarith/Ring imports.