proposition: Fact square_4_simpl x m : (4*(x*x) = Z.of_nat m*Z.of_nat m)%Z -> { n | m = 2*n /\ (x = Z.of_nat n \/ (x = - Z.of_nat n)%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 ]. + destruct Z_of_nat_complete_inf with x as (k & ->). * generalize (Zle_0_nat m); lia. * exists k; split; auto. apply Nat2Z.inj. rewrite Nat2Z.inj_mul, <- H; auto. + destruct (Z_of_nat_complete_inf (Z.opp x)) as (k & Hk). * generalize (Zle_0_nat m); lia. * exists k; split. - apply Nat2Z.inj. rewrite Nat2Z.inj_mul, <- H, <- Hk; ring. - right; rewrite <- Hk; ring. Qed.
imports: Arith ZArith Lia List Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list gcd prime php utils_nat) Undecidability.H10.ArithLibs(Zp)