proposition: Fact square_4_simpl' x m : (4*(x*x) = Z.of_nat (2*m)*Z.of_nat (2*m) -> x = Z.of_nat m \/ x = - Z.of_nat m)%Z.
proof: Proof. intros H. replace (4*(x*x))%Z with ((2*x)*(2*x))%Z in H by ring. apply Zsquare_inj in H. destruct H as [ H | H ]; rewrite Nat2Z.inj_mul in H; change (Z.of_nat 2) with 2%Z in H; 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)