↦ xy/2# on the positive rationals. So we have another monoid structure on the positive rational numbers.
*)
-inline procedural "cic:/CoRN/model/monoids/QSposmonoid/QTWOpos_is_rht_unit.con".
+inline procedural "cic:/CoRN/model/monoids/QSposmonoid/QTWOpos_is_rht_unit.con" as lemma.
-inline procedural "cic:/CoRN/model/monoids/QSposmonoid/QTWOpos_is_lft_unit.con".
+inline procedural "cic:/CoRN/model/monoids/QSposmonoid/QTWOpos_is_lft_unit.con" as lemma.
-inline procedural "cic:/CoRN/model/monoids/QSposmonoid/Qpos_multdiv2_is_CMonoid.con".
+inline procedural "cic:/CoRN/model/monoids/QSposmonoid/Qpos_multdiv2_is_CMonoid.con" as definition.
-inline procedural "cic:/CoRN/model/monoids/QSposmonoid/Qpos_multdiv2_as_CMonoid.con".
+inline procedural "cic:/CoRN/model/monoids/QSposmonoid/Qpos_multdiv2_as_CMonoid.con" as definition.