Non-example of a monoid: ⟨N+,+⟩

There is no right unit for the addition on the positive natural numbers.

Lemma no_rht_unit_Npos : forall y : N+, ~ is_rht_unit (S:=Npos) Npos_plus y.

Therefore the set of positive natural numbers doesn't form a group with addition.

Lemma no_monoid_Npos : forall y : N+, ~ is_CMonoid Npos_as_CSemiGroup y.