Example of a semi-group: ⟨Q+,×⟩

The positive rationals form with the multiplication a CSemiGroup.

Definition Qpos_mult_as_CSemiGroup := Build_CSemiGroup
 Qpos_as_CSetoid Qpos_mult_is_bin_fun associative_Qpos_mult.