proposition: Lemma Nrel_prime_eqmod m a b : m <> 0 -> a mod m = b mod m -> Nrel_prime m a -> Nrel_prime m b.
proof: Proof. intros mz ab ma x xm xb. apply (ma x xm); clear ma. destruct (le_lt_dec a b) as [le|lt]. - rewrite eqmod_div in ab; auto. destruct xb as (k & ->). destruct xm as (l & ->). destruct ab as (m & em). exists (k - m * l). replace ((k - m * l) * x) with (k * x - m * (l * x)). lia. rewrite Nat.mul_sub_distr_r. lia. - symmetry in ab. rewrite eqmod_div in ab; auto. 2:lia. destruct xb as (k & ->). destruct xm as (l & ->). destruct ab as (m & em). exists (m * l + k). replace ((m * l + k) * x) with (k * x + m * (l * x)). lia. rewrite Nat.mul_add_distr_r. lia. Qed.
imports: Coq(Arith Euclid Compare Lia)