CoRN.old.Npos_no_monoid

Require Export Npossemigroup.
Require Import CMonoids.

Non-example of a monoid: ⟨Npos,[+]⟩

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

Lemma no_rht_unit_Npos : ∀ y : Npos, ¬ is_rht_unit (S:=Npos) Npos_plus y.
Proof.
unfold is_rht_unit in |- ×.
intro y.
case y.
intros scs_elem scs_prf.
apply no_rht_unit_Npos1.
Qed.

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

Lemma no_monoid_Npos : ∀ y : Npos, ¬ is_CMonoid Npos_as_CSemiGroup y.
Proof.
intro y.
red in |- ×.
intro H.
set (H0 := no_rht_unit_Npos y) in ×.
apply H0.
apply (runit Npos_as_CSemiGroup).
exact H.
Qed.