proposition: Fact remarkable_id1_Z (a b : Z) : ((a+b)*(a+b) = a*a + 2*a*b + b*b)%Z.
proof: Proof. 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)