proposition: Lemma Zmod_relprime_inv : forall m a : Z, (m > 1)%Z -> Zrelprime a m -> ((a * Zgcd_coeff_a a m) mod m)%Z = 1%Z.
proof: Proof. intros m a Hm H1. unfold Zrelprime in H1. generalize (Zgcd_lin_comb a m). intro Hlc. rewrite H1 in Hlc. rewrite (Zmult_comm (Zgcd_coeff_a a m) a) in Hlc. assert (Hqr : (a * Zgcd_coeff_a a m)%Z = (- Zgcd_coeff_b a m * m + 1)%Z). rewrite Zplus_comm. rewrite Hlc. rewrite <- Zplus_assoc. rewrite Zopp_mult_distr_l_reverse. auto with zarith. set (Hdivmod:=Z_div_mod_eq_full (a * Zgcd_coeff_a a m) m). rewrite (Zmult_comm m (a * Zgcd_coeff_a a m / m)) in Hdivmod. apply (Zdiv_remainder_unique _ _ _ _ (- Zgcd_coeff_b a m) 1 Hdivmod). apply Z_mod_lt. auto with zarith. exact Hqr. auto with zarith. Qed.
imports: CoRN.model.Zmod.ZGcd