Example of a group: ⟨Q+,×⟩

The positive rational numbers form a multiplicative group.

Lemma Qpos_is_CGroup : is_CGroup Qpos_mult_as_CMonoid Qpos_inv_op.

Definition Qpos_as_CGroup := Build_CGroup
 Qpos_mult_as_CMonoid Qpos_inv_op Qpos_is_CGroup.