proposition: Lemma Zmod_sqrt_eq_compat : forall p i j, prime p -> (0 <= i -> 0 <= j -> 2 * i < p -> 2 * j < p -> i * i ≡ j * j [p] -> i = j)%Z.
proof: Proof. intros p i j Pp Pi Pj Bi Bj ES. destruct (Z.eq_dec ((i + j) mod p) 0) as [ E | E ]. cut (i + j = 0); [ lia | ]. cut (i + j < p); [ intros H | lia ]. rewrite <- E; symmetry; apply Zmod_small. lia. destruct (modular_inverse _ _ Pp E) as (a, Ha). cut (i ≡ j [p]). intros M; red in M. rewrite (Zmod_small i p), (Zmod_small j p) in M; lia. apply eqm_minus_0. replace (i - j) with ((i - j) * 1) by ring. rewrite <- Ha. apply eqm_minus_0 in ES. replace 0 with (0 * a) by ring. rewrite <- ES. apply eq_eqm; ring. Qed.
imports: ZArith Lia Znumtheory Natsets MyNat Ztools Zeqm Znumfacts