proposition: Lemma modular_mult_inj : forall p n, prime p -> ~ (0 ≡ n [p]) -> forall x y, x * n ≡ y * n [p] -> x ≡ y [p].
proof: Proof. intros p n Pp Nn x y E. apply eqm_minus_0, divide_eqm; notzero. assert (D : (p | (x - y) * n)). apply divide_eqm; notzero. ring_simplify. rewrite E. red; f_equal; ring. destruct (prime_mult _ Pp _ _ D) as [D1|D2]; auto. exfalso; apply Nn. symmetry; apply divide_eqm; auto. notzero. Qed.
imports: ZArith Lia Znumtheory Natsets MyNat Ztools Zeqm