There is no right unit for the addition on the positive natural numbers.
*)
-inline procedural "cic:/CoRN/model/non_examples/Npos_no_monoid/no_rht_unit_Npos.con".
+inline procedural "cic:/CoRN/model/non_examples/Npos_no_monoid/no_rht_unit_Npos.con" as lemma.
(*#* Therefore the set of positive natural numbers doesn't form a group with
addition.
*)
-inline procedural "cic:/CoRN/model/non_examples/Npos_no_monoid/no_monoid_Npos.con".
+inline procedural "cic:/CoRN/model/non_examples/Npos_no_monoid/no_monoid_Npos.con" as lemma.