One is the unit for multiplication on positive integers. Therefore the positive rational numbers together with the multiplication are a CMonoid.
*)
-inline procedural "cic:/CoRN/model/monoids/Qposmonoid/QONEpos_is_rht_unit.con".
+inline procedural "cic:/CoRN/model/monoids/Qposmonoid/QONEpos_is_rht_unit.con" as lemma.
-inline procedural "cic:/CoRN/model/monoids/Qposmonoid/QONEpos_is_lft_unit.con".
+inline procedural "cic:/CoRN/model/monoids/Qposmonoid/QONEpos_is_lft_unit.con" as lemma.
-inline procedural "cic:/CoRN/model/monoids/Qposmonoid/Qpos_mult_is_CMonoid.con".
+inline procedural "cic:/CoRN/model/monoids/Qposmonoid/Qpos_mult_is_CMonoid.con" as definition.
-inline procedural "cic:/CoRN/model/monoids/Qposmonoid/Qpos_mult_as_CMonoid.con".
+inline procedural "cic:/CoRN/model/monoids/Qposmonoid/Qpos_mult_as_CMonoid.con" as definition.