Example of a monoid: ⟨N+,[*]⟩

One is the right unit as well as the left unit of the multiplication on the positive natural numbers.

Lemma rhtunitNpos : is_rht_unit Npos_mult ONEpos.

Lemma lftunitNpos : is_lft_unit Npos_mult ONEpos.

So, the positive natural numbers with multiplication form a CMonoid.

Definition Nposmult_is_CMonoid := Build_is_CMonoid
 Nposmult_as_CSemiGroup ONEpos rhtunitNpos lftunitNpos.

Definition Nposmult_as_CMonoid := Build_CMonoid
 Nposmult_as_CSemiGroup ONEpos Nposmult_is_CMonoid.