proposition: Lemma Zmod_plus_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. exact Hm. 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 Zopp_plus_distr; repeat rewrite Z.opp_involutive. rewrite (Zplus_comm (a + b) (- (m * ((a + b) / m)))). repeat rewrite <- Zplus_assoc. apply Zdivides_plus_elim. auto with zarith. rewrite (Zplus_assoc (m * (a / m)) (- b) (m * (b / m))). rewrite (Zplus_comm (m * (a / m)) (- b)). rewrite <- (Zplus_assoc (- b) (m * (a / m)) (m * (b / m))). rewrite (Zplus_assoc (- a) (- b) (m * (a / m) + m * (b / m))). rewrite <- Zopp_plus_distr. repeat rewrite Zplus_assoc. rewrite Zplus_opp_r. 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