proposition: Lemma Zm_mult_onel : forall x:Zm_cabgroup, (Zm_mult_op 1 x)[=]x.
proof: Proof. intro. astepl (Zm_mult_op x 1). exact (Zm_mult_one x). exact (Zm_mult_commutative x 1). Qed.
imports: CoRN.model.Zmod.ZMod CoRN.algebra.CFields