multiplication and it satisfies the distributive law, it is a ring.
*)
-inline procedural "cic:/CoRN/model/rings/Qring/Q_mult_plus_is_dist.con".
+inline procedural "cic:/CoRN/model/rings/Qring/Q_mult_plus_is_dist.con" as lemma.
-inline procedural "cic:/CoRN/model/rings/Qring/Q_is_CRing.con".
+inline procedural "cic:/CoRN/model/rings/Qring/Q_is_CRing.con" as definition.
-inline procedural "cic:/CoRN/model/rings/Qring/Q_as_CRing.con".
+inline procedural "cic:/CoRN/model/rings/Qring/Q_as_CRing.con" as definition.
(*#* The following lemmas are used in the proof that [Q] is Archimeadian.
*)
-inline procedural "cic:/CoRN/model/rings/Qring/injz_Nring.con".
+inline procedural "cic:/CoRN/model/rings/Qring/injz_Nring.con" as lemma.
-inline procedural "cic:/CoRN/model/rings/Qring/injZ_eq.con".
+inline procedural "cic:/CoRN/model/rings/Qring/injZ_eq.con" as lemma.
-inline procedural "cic:/CoRN/model/rings/Qring/nring_Q.con".
+inline procedural "cic:/CoRN/model/rings/Qring/nring_Q.con" as lemma.