Example of a monoid: ⟨Q+,×⟩
One is the unit for multiplication on positive integers. Therefore the positive rational numbers together with the multiplication are a CMonoid.Lemma QONEpos_is_rht_unit : is_rht_unit Qpos_mult_is_bin_fun (1#1)%Qpos.
Lemma QONEpos_is_lft_unit : is_lft_unit Qpos_mult_is_bin_fun (1#1)%Qpos.
Definition Qpos_mult_is_CMonoid := Build_is_CMonoid
Qpos_mult_as_CSemiGroup _ QONEpos_is_rht_unit QONEpos_is_lft_unit.
Definition Qpos_mult_as_CMonoid := Build_CMonoid
Qpos_mult_as_CSemiGroup _ Qpos_mult_is_CMonoid.