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