proposition: Lemma Zm_is_CRing : (is_CRing Zm_cabgroup 1 Zm_mult_op).
proof: Proof. apply Build_is_CRing with Zm_mult_assoc. exact Zm_mult_monoid. exact Zm_mult_commutative. exact Zm_mult_plus_dist. exact Zm_non_triv. Qed.
imports: CoRN.model.Zmod.ZMod CoRN.algebra.CFields