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