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

⟨Z,+⟩


Lemma Zplus_is_CSemiGroup: (is_CSemiGroup Z_as_CSetoid Zplus_is_bin_fun).

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).

Definition Z_mul_as_CSemiGroup := Build_CSemiGroup _ Zmult_is_bin_fun Zmult_is_assoc.