proposition: Fact Zsquare_inj x y : (x*x = y*y -> { x = y } + { - x = y } )%Z.
proof: Proof. intros H. assert ( (x+y)*(x-y) = 0 )%Z as E. { rewrite Z.mul_sub_distr_l, !Z.mul_add_distr_r, H; ring. } apply Zmult_integral in E. destruct (Z.eq_dec x y); auto. right; lia. Qed.
imports: Arith ZArith Lia List Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list gcd prime php utils_nat) Undecidability.H10.ArithLibs(Zp)