proposition: Lemma Zmod_lin_comb : forall m a : Z, (m > 0)%Z -> (Zgcd a m < m)%Z -> ((a * Zgcd_coeff_a a m) mod m)%Z = Zgcd a m.
proof: Proof. intros m a Hm Hgcd. generalize (Zgcd_lin_comb a m); intro Hlincomb. rewrite (Z_div_mod_eq_full (Zgcd_coeff_a a m * a) m) in Hlincomb. rewrite Zmult_comm in Hlincomb. rewrite Zplus_comm in Hlincomb. rewrite Zplus_assoc in Hlincomb. rewrite <- Zmult_plus_distr_l in Hlincomb. replace (Zgcd a m) with (Zgcd a m mod m)%Z. rewrite Hlincomb. rewrite Zmod_plus_compat; auto. rewrite Zmod_Zmod; auto. rewrite <- Zmod_plus_compat; auto. apply Zmod_minus_intro; auto. set (u := Zgcd_coeff_a a m). set (v := Zgcd_coeff_b a m). rewrite (Zplus_comm ((v + u * a / m) * m) (u * a)). unfold Zminus in |- *. rewrite Zopp_plus_distr. rewrite Zplus_assoc. rewrite (Zmult_comm a u). rewrite Zplus_opp_r. rewrite Zplus_0_l. rewrite <- Zopp_mult_distr_l_reverse. apply Zmod_multiple; auto. apply Zmod_small; auto. auto with zarith. Qed.
imports: CoRN.model.Zmod.ZGcd