proposition: Lemma Zmodeq_mod_intro : forall a b : Z, Zmodeq (a mod m) (b mod m) -> Zmodeq a b.
proof: Proof. intros a b H. apply Zmodeq_eqmod. rewrite <- (Zmod_Zmod m a); auto with zarith. rewrite <- (Zmod_Zmod m b); auto with zarith. Qed.
imports: CoRN.model.Zmod.ZGcd