proposition: Lemma Zp_small_repr m (Hm : m <> 0) x : exists y, Z2Zp Hm x = Z2Zp Hm y /\ (4*(y*y) <= Z.of_nat m * Z.of_nat m)%Z.
proof: Proof. destruct (euclid_2 m) as (p & [ H | H ]). + destruct (Zp_repr_interval Hm (- Z.of_nat p)%Z (Z.of_nat p) x) as (y & H1 & H2). * rewrite H, Nat2Z.inj_mul; simpl Z_of_nat; lia. * exists y; split; auto. rewrite H, Nat2Z.inj_mul. simpl Z.of_nat. replace (2*Z.of_nat p*(2*Z.of_nat p))%Z with (4*(Z.of_nat p*Z.of_nat p))%Z by ring. nia. + destruct (Zp_repr_interval Hm (- Z.of_nat p)%Z (1+Z.of_nat p) x) as (y & H1 & H2). * rewrite H, Nat2Z.inj_add, Nat2Z.inj_mul; simpl Z_of_nat; lia. * exists y; split; auto. apply Z.le_trans with (Z.of_nat (2*p) * Z.of_nat (2*p))%Z. - rewrite Nat2Z.inj_mul. simpl Z.of_nat. replace (2*Z.of_nat p*(2*Z.of_nat p))%Z with (4*(Z.of_nat p*Z.of_nat p))%Z by ring. nia. - apply Zsquare_bound; subst. rewrite !Nat2Z.inj_add, !Nat2Z.inj_mul; simpl Z.of_nat; 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)