proposition: Lemma Zmodeq_rem : forall a : Z, Zmodeq a (a mod m).
proof: Proof. intros. unfold Zmodeq in |- *. exists (a / m)%Z. rewrite Zmult_comm. generalize (Z_div_mod_eq_full a m). auto with zarith. Qed.
imports: CoRN.model.Zmod.ZGcd