CoRN.model.semigroups.Qpossemigroup

Require Export Qpossetoid.
Require Export CSemiGroups.

Example of a semi-group: ⟨Qpos,[*]⟩

The positive rationals form with the multiplication a CSemiGroup.