proposition: Fact Euler_squares x y a1 b1 c1 d1 a2 b2 c2 d2 : (x = four_squares a1 b1 c1 d1 -> y = four_squares a2 b2 c2 d2 -> x*y = four_squares (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))%Z.
proof: Proof. intros -> ->; ring. Qed.
imports: Arith ZArith Lia List Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list gcd prime php utils_nat) Undecidability.H10.ArithLibs(Zp)