proposition: Lemma Zm_is_CSetoid : (is_CSetoid _ ZModeq ZModap).
proof: Proof. apply Build_is_CSetoid. exact Zmodap_irreflexive. exact Zmodap_symmetric. exact Zmodap_cotransitive. exact Zmodap_tight_apart. Qed.
imports: CoRN.model.Zmod.ZMod CoRN.algebra.CFields