Example of a group: ⟨Q+, (x,y) ↦ xy/2⟩

The positive rationals form with the operation (x,y) ↦ xy/2 a CGroup.

Lemma Qpos_multdiv2_is_CGroup : is_CGroup Qpos_multdiv2_as_CMonoid divmult4.

Definition Qpos_multdiv2_as_CGroup := Build_CGroup
 Qpos_multdiv2_as_CMonoid divmult4 Qpos_multdiv2_is_CGroup.