Examples of a monoid: ⟨Q,+⟩ and ⟨Q,[*]⟩

⟨Q,+⟩

The rational numbers form with addition a CMonoid. 0Q is the unit.

Lemma ZEROQ_as_rht_unit3 : is_rht_unit (S:=Q_as_CSetoid) Qplus_is_bin_fun 0.

Lemma ZEROQ_as_lft_unit3 : is_lft_unit (S:=Q_as_CSetoid) Qplus_is_bin_fun 0.

Definition Q_is_CMonoid := Build_is_CMonoid
 Q_as_CSemiGroup _ ZEROQ_as_rht_unit3 ZEROQ_as_lft_unit3.

Definition Q_as_CMonoid := Build_CMonoid Q_as_CSemiGroup _ Q_is_CMonoid.

Canonical Structure Q_as_CMonoid.

⟨Q,[*]⟩

Also with multiplication Q forms a CMonoid. Here, the unit is 1Q.

Lemma ONEQ_as_rht_unit : is_rht_unit (S:=Q_as_CSetoid) Qmult_is_bin_fun 1.

Lemma ONEQ_as_lft_unit : is_lft_unit (S:=Q_as_CSetoid) Qmult_is_bin_fun 1.

Definition Q_mul_is_CMonoid := Build_is_CMonoid
 Q_mul_as_CSemiGroup _ ONEQ_as_rht_unit ONEQ_as_lft_unit.

Definition Q_mul_as_CMonoid := Build_CMonoid
 Q_mul_as_CSemiGroup _ Q_mul_is_CMonoid.