proposition: Theorem lagrange_theorem_nat : forall n, exists a b c d, Z.of_nat n = a*a+b*b+c*c+d*d.
proof: Proof. induction n as [ | | p Hp | x y Hx Hy ] using prime_rect. + exists 0, 0, 0, 0; auto. + exists 1, 0, 0, 0; auto. + apply lagrange_prime; auto. + destruct Hx as (a1 & b1 & c1 & d1 & H1). destruct Hy as (a2 & b2 & c2 & d2 & H2). subst. exists (a1*a2+b1*b2+c1*c2+d1*d2), (a1*b2-b1*a2+d1*c2-c1*d2), (a1*c2-c1*a2+b1*d2-d1*b2), (a1*d2-d1*a2+c1*b2-b1*c2). rewrite Nat2Z.inj_mul; apply Euler_squares; auto. Qed.
imports: Arith ZArith Lia List Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list gcd prime php utils_nat) Undecidability.H10.ArithLibs(Zp)