CoRN.model.semigroups.QSpossemigroup

Require Export Qpossetoid.
Require Import CSemiGroups.

Example of a semi-group: ⟨Qpos,(x,y) ↦ xy/2⟩

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