proposition: Lemma Zp_square_zero m (Hm : m <> 0) (Hm2 : m*m <> 0) x : Z2Zp Hm x = Zp_zero Hm -> Z2Zp Hm2 (x*x) = Zp_zero Hm2.
proof: Proof. intros H. apply Z2Zp_zero_inv in H. destruct H as (v & ->). replace (Z.of_nat m*v*(Z.of_nat m*v))%Z with (Z.of_nat m*Z.of_nat m*(v*v))%Z by ring. now rewrite <- Nat2Z.inj_mul, Z2Zp_mult, Z2Zp_of_nat, nat2Zp_p, Zp_mult_zero. Qed.
imports: Arith ZArith Lia List Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list gcd prime php utils_nat) Undecidability.H10.ArithLibs(Zp)