CoRN.model.semigroups.Nsemigroup

Require Export Nsetoid.
Require Import CSemiGroups.

Example of a semi-group: ⟨nat,[+]⟩

Because addition is associative, the natural numbers form a CSemiGroup.

Definition nat_as_CSemiGroup := Build_CSemiGroup _ plus_is_bin_fun plus_is_assoc.

Canonical Structure nat_as_CSemiGroup.

Lemma Nmult_is_CSemiGroup : is_CSemiGroup nat_as_CSetoid mult_as_bin_fun.
Proof.
unfold is_CSemiGroup in |- ×.
unfold associative in |- ×.
unfold mult_as_bin_fun in |- ×.
simpl in |- ×.
auto with arith.
Qed.

Definition Nmult_as_CSemiGroup := Build_CSemiGroup
nat_as_CSetoid mult_as_bin_fun Nmult_is_CSemiGroup.