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

⟨N+,+⟩

The positive natural numbers form together with addition a subsemigroup of the semigroup of the natural numbers with addition.

Definition Npos_as_CSemiGroup := Build_SubCSemiGroup
 nat_as_CSemiGroup NposP plus_resp_Npos.

⟨N+,[*]⟩

Also together with multiplication, the positive numbers form a semigroup.

Lemma Nposmult_is_CSemiGroup : is_CSemiGroup N+ Npos_mult.

Definition Nposmult_as_CSemiGroup := Build_CSemiGroup
 N+ Npos_mult Nposmult_is_CSemiGroup.