proposition: Lemma modular_inverse : forall p x, prime p -> ~(x ≡ 0 [p]) -> { y | x * y ≡ 1 [p] }.
proof: Proof. intros p x Pp Nd. assert (rel_prime (x mod p) p). apply Pp. assert (A : p > 0) by notzero; pose proof Z_mod_lt x p A. unfold eqm in Nd; rewrite Zmod_0_l in Nd. lia. destruct (rel_prime_bezout _ _ H) as (u, (v, Huv)). exists u. rewrite <- Huv. assert (REW : x mod p ≡ x [p]) by (red; rewrite Zmod_mod; auto) . rewrite REW. apply eqm_minus_0. ring_simplify. apply divide_eqm. notzero. exists (- v); auto. Qed.
imports: ZArith Lia Znumtheory Natsets MyNat Ztools Zeqm