The rational numbers form with addition a CMonoid. [QZERO] is the unit.
*)
-inline procedural "cic:/CoRN/model/monoids/Qmonoid/ZEROQ_as_rht_unit3.con".
+inline procedural "cic:/CoRN/model/monoids/Qmonoid/ZEROQ_as_rht_unit3.con" as lemma.
-inline procedural "cic:/CoRN/model/monoids/Qmonoid/ZEROQ_as_lft_unit3.con".
+inline procedural "cic:/CoRN/model/monoids/Qmonoid/ZEROQ_as_lft_unit3.con" as lemma.
-inline procedural "cic:/CoRN/model/monoids/Qmonoid/Q_is_CMonoid.con".
+inline procedural "cic:/CoRN/model/monoids/Qmonoid/Q_is_CMonoid.con" as definition.
-inline procedural "cic:/CoRN/model/monoids/Qmonoid/Q_as_CMonoid.con".
+inline procedural "cic:/CoRN/model/monoids/Qmonoid/Q_as_CMonoid.con" as definition.
(*#* ***$\langle$#⟨#[Q],[[*]]$\rangle$#⟩#
Also with multiplication Q forms a CMonoid. Here, the unit is [QONE].
*)
-inline procedural "cic:/CoRN/model/monoids/Qmonoid/ONEQ_as_rht_unit.con".
+inline procedural "cic:/CoRN/model/monoids/Qmonoid/ONEQ_as_rht_unit.con" as lemma.
-inline procedural "cic:/CoRN/model/monoids/Qmonoid/ONEQ_as_lft_unit.con".
+inline procedural "cic:/CoRN/model/monoids/Qmonoid/ONEQ_as_lft_unit.con" as lemma.
-inline procedural "cic:/CoRN/model/monoids/Qmonoid/Q_mul_is_CMonoid.con".
+inline procedural "cic:/CoRN/model/monoids/Qmonoid/Q_mul_is_CMonoid.con" as definition.
-inline procedural "cic:/CoRN/model/monoids/Qmonoid/Q_mul_as_CMonoid.con".
+inline procedural "cic:/CoRN/model/monoids/Qmonoid/Q_mul_as_CMonoid.con" as definition.