proposition: Lemma Zmod_minus_intro : forall m a b : Z, (m > 0)%Z -> ((a - b) mod m)%Z = 0%Z -> (a mod m)%Z = (b mod m)%Z.
proof: Proof. intros m a b Hm H0. assert (Hdiv : Zdivides m (a - b)); auto with zarith. elim Hdiv; intros q Hq. replace a with (q * m + b)%Z; auto with zarith. apply Zmod_cancel_multiple. assumption. Qed.
imports: CoRN.model.Zmod.ZGcd