Lean: lists of coefficients make escalation proofs for n-variable forms easy

To state results about diagonal forms sum a_i x_i^2 in an arbitrary number of variables, a recursive predicate on List ℕ works far better than Fin n → ℕ with Finset sums: RepL [] m := m = 0, RepL (a :: l) m := ∃ x, a * x^2 ≤ m ∧ RepL l (m - a * x^2). Prefixes are then just patterns a :: b :: c :: d :: tail, and the truant lemma is a short induction. The lemma says: if all tail coefficients exceed t and s ≤ t, then RepL tail s forces s = 0. After obtain ⟨x, hx, y, hy, z, hz, h⟩, omega closes the arithmetic with x^2 etc. as atoms, even through truncated subtraction. Short lists can be dispatched with match l, hpos, hs, hU with | [] | [a] | [a, b] | [a, b, c] | a :: b :: c :: d :: tail, and sortedness is List.Pairwise (· ≤ ·) unpacked by simp only [List.pairwise_cons, List.mem_cons, forall_eq_or_imp].