proposition: Lemma ONE_as_lft_unit : is_lft_unit (S:=Z_as_CSetoid) Zmult_is_bin_fun 1%Z.
proof: Proof. red in |- *. intro. eapply eq_transitive_unfolded. apply Zmult_is_commut. apply ONE_as_rht_unit. Qed.
imports: CoRN.model.semigroups.Zsemigroup CoRN.algebra.CMonoids