proposition: Lemma Zm_mult_commutative: forall x y:Zm_cabgroup, (Zm_mult_op x y) [=] (Zm_mult_op y x).
proof: Proof. intros x y. simpl. unfold ZModeq; unfold Zm_mult. rewrite Zmult_comm. apply Zmodeq_refl. Qed.
imports: CoRN.model.Zmod.ZMod CoRN.algebra.CFields