proposition: Lemma Zm_is_CGroup : (is_CGroup _ Zm_opp_op).
proof: Proof. unfold is_CGroup. unfold is_inverse. simpl. unfold ZModeq; unfold Zm_plus; unfold Zm_opp. intro. rewrite Zplus_opp_r. rewrite Zplus_opp_l. auto with zarith. Qed.
imports: CoRN.model.Zmod.ZMod CoRN.algebra.CFields