proposition: Lemma lagrange_fun_spec (n : Z) : (let (ab, cd) := lagrange_fun n in let (a, b) := ab in let (c, d) := cd in Z.abs n = a * a + b * b + c * c + d * d).
proof: Proof. unfold lagrange_fun. destruct (lagrange_4_square_theorem (Z.abs n) (Zabs_pos n)) as (a, (b, (c, (d, pr)))). exact pr. Qed.
imports: ZArith Lia Znumtheory Natsets MyNat Ztools Zeqm Znumfacts