proposition: Lemma Zmod_mult_compat : forall m a b : Z, (m > 0)%Z -> ((a * b) mod m)%Z = ((a mod m * (b mod m)) mod m)%Z.
proof: Proof. intros m a b Hm. rewrite <- (Zmod_Zmod m (a * b) Hm). apply Zmod_minus_intro; auto. apply Zmod0_Zdivides. auto with zarith. replace (a mod m)%Z with (a - m * (a / m))%Z. replace (b mod m)%Z with (b - m * (b / m))%Z. replace ((a * b) mod m)%Z with (a * b - m * (a * b / m))%Z. unfold Zminus in |- *; repeat rewrite Zplus_assoc. repeat rewrite Zmult_plus_distr_l. repeat rewrite Zmult_plus_distr_r. repeat rewrite Zopp_plus_distr; repeat rewrite Z.opp_involutive. rewrite (Zplus_comm (a * b)). repeat rewrite <- Zplus_assoc. apply Zdivides_plus_elim. auto with zarith. repeat rewrite Zplus_assoc. rewrite Zplus_opp_r. repeat rewrite Zopp_mult_distr_l_reverse; repeat rewrite Zopp_mult_distr_r; repeat rewrite Z.opp_involutive. simpl in |- *. apply Zdivides_plus_elim; auto with zarith. generalize (Z_div_mod_eq_full (a * b) m); auto with zarith. generalize (Z_div_mod_eq_full b m); auto with zarith. generalize (Z_div_mod_eq_full a m); auto with zarith. Qed.
imports: CoRN.model.Zmod.ZGcd