CoRN.model.semigroups.Qsemigroup

Require Export Qsetoid.
Require Import CSemiGroups.

Examples of semi-groups: ⟨Q,[+]⟩ and ⟨Q,[*]⟩

⟨Q,[+]⟩

Definition Q_as_CSemiGroup := Build_CSemiGroup _ Qplus_is_bin_fun Qplus_is_assoc.

Canonical Structure Q_as_CSemiGroup.

⟨Q,[*]⟩

Definition Q_mul_as_CSemiGroup := Build_CSemiGroup _ Qmult_is_bin_fun Qmult_is_assoc.