proposition: Lemma Zmod_minus_elim : forall m a b : Z, (m > 0)%Z -> (a mod m)%Z = (b mod m)%Z -> ((a - b) mod m)%Z = 0%Z.
proof: Proof. intros m a b Hm Heq. unfold Zminus in |- *. rewrite (Zmod_plus_compat m a (- b) Hm). rewrite Heq. rewrite Zmod_opp_elim; auto. rewrite <- (Zmod_plus_compat m b (m - b mod m) Hm). unfold Zminus in |- *. rewrite Zplus_assoc. rewrite (Zplus_comm b m). rewrite <- Zplus_assoc. fold (b - b mod m)%Z in |- *. replace (b - b mod m)%Z with (b / m * m)%Z. rewrite Zplus_comm. rewrite Zmod_cancel_multiple; auto. apply Zmod_same; auto. set (q := (b / m)%Z); set (r := (b mod m)%Z). rewrite (Z_div_mod_eq_full b m). fold q in |- *; fold r in |- *. rewrite Zmult_comm. unfold Zminus in |- *. rewrite <- Zplus_assoc. rewrite Zplus_opp_r. auto with zarith. Qed.
imports: CoRN.model.Zmod.ZGcd