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

There is no inverse function for the natural numbers with addition.

Lemma no_inverse_nat_plus : forall inv : CSetoid_un_op nat_as_CSetoid,
 ~ is_inverse (csg_op (c:=nat_as_CSemiGroup)) 0 2 (inv 2).

Hence they do not form a CGroup.

Lemma no_group_nat_plus : forall inv : CSetoid_un_op nat_as_CMonoid,
 ~ is_CGroup nat_as_CMonoid inv.