CoRN.model.semigroups.Zsemigroup

Require Export Zsetoid.
Require Export CSemiGroups.

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

⟨Z,[+]⟩

Lemma Zplus_is_CSemiGroup: (is_CSemiGroup Z_as_CSetoid Zplus_is_bin_fun).
Proof.
unfold is_CSemiGroup.
exact Zplus_is_assoc.
Qed.

Definition Z_as_CSemiGroup := Build_CSemiGroup _ Zplus_is_bin_fun Zplus_is_assoc.

Canonical Structure Z_as_CSemiGroup.

The term Z_as_CSemiGroup is of type CSemiGroup. Hence we have proven that Z is a constructive semi-group.

⟨Z,[*]⟩

Lemma Zmult_is_CSemiGroup: (is_CSemiGroup Z_as_CSetoid Zmult_is_bin_fun).
Proof.
unfold is_CSemiGroup.
exact Zmult_is_assoc.
Qed.

Definition Z_mul_as_CSemiGroup := Build_CSemiGroup _ Zmult_is_bin_fun Zmult_is_assoc.