proposition: Fact half_modulus_lemma' x : Z2Zp H2m x = nat2Zp H2m m \/ (Z2Zp H2m x = Zp_opp H2m (nat2Zp H2m m))%Z -> Z2Zp Hm2 (x*x) = nat2Zp Hm2 (m*m).
proof: Proof. intros []; 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)