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

There is no inverse for multiplication on the positive natural numbers.

Lemma no_inverse_Nposmult : forall inv : CSetoid_un_op N+,
 ~ is_inverse Npos_mult ONEpos TWOpos (inv TWOpos).

Hence the natural numbers with multiplication do not form a group.

Lemma no_group_Nposmult : forall inv : CSetoid_un_op Nposmult_as_CMonoid,
 ~ is_CGroup Nposmult_as_CMonoid inv.