proposition: Lemma Zmodeq_modeq : forall a b : Z, Zmodeq a b -> (a mod m)%Z = (b mod m)%Z.
proof: Proof. intros a b H. apply Zmod_minus_intro. auto with zarith. unfold Zmodeq in H. apply Zmod0_Zdivides. intro Hfalse; inversion Hfalse. assumption. Qed.
imports: CoRN.model.Zmod.ZGcd