CoRN.model.monoids.Nposmonoid

Require Export Npossemigroup.
Require Import CMonoids.

Example of a monoid: ⟨Npos,[*]⟩

One is the right unit as well as the left unit of the multiplication on the positive natural numbers.

Lemma rhtunitNpos : is_rht_unit Npos_mult ONEpos.
Proof.
unfold is_rht_unit in |- ×.
unfold Npos_mult in |- ×.
intro x.
case x.
simpl in |- ×.
intros scs_elem H.
auto with arith.
Qed.

Lemma lftunitNpos : is_lft_unit Npos_mult ONEpos.
Proof.
unfold is_rht_unit in |- ×.
unfold Npos_mult in |- ×.
intro x.
case x.
simpl in |- ×.
intros scs_elem H.
auto with arith.
Qed.

So, the positive natural numbers with multiplication form a CMonoid.