Example of an abelian group: ⟨Q+,×⟩

The positive rationals form with the multiplication a CAbgroup.

Definition Qpos_mult_is_CAbGroup : is_CAbGroup Qpos_as_CGroup.
Qed.

Definition Qpos_mult_as_CAbGroup := Build_CAbGroup
 Qpos_as_CGroup Qpos_mult_is_CAbGroup.