proposition: Fact half_modulus_lemma x y : Z2Zp H2m x = Z2Zp H2m y -> y = Z.of_nat m \/ y = (- Z.of_nat m)%Z -> Z2Zp Hm2 (x*x) = nat2Zp Hm2 (m*m).
proof: Proof. intros H1 H2. apply half_modulus_lemma'. rewrite H1. destruct H2; subst y; [ left | right ]. + rewrite Z2Zp_of_nat; auto. + rewrite Z2Zp_opp, Z2Zp_of_nat; 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)