Example of a monoid: ⟨Q+, (x,y) ↦ xy/2⟩
Two is the unit of the operation (x,y) ↦ xy/2 on the positive rationals. So we have another monoid structure on the positive rational numbers.Lemma QTWOpos_is_rht_unit : is_rht_unit multdiv2 (2#1)%Qpos.
Lemma QTWOpos_is_lft_unit : is_lft_unit multdiv2 (2#1)%Qpos.
Definition Qpos_multdiv2_is_CMonoid := Build_is_CMonoid
Qpos_multdiv2_as_CSemiGroup _ QTWOpos_is_rht_unit QTWOpos_is_lft_unit.
Definition Qpos_multdiv2_as_CMonoid := Build_CMonoid
Qpos_multdiv2_as_CSemiGroup _ Qpos_multdiv2_is_CMonoid.