A variant of [0_S] from the standard library
*)
-inline procedural "cic:/CoRN/model/structures/Nsec/S_O.con".
+inline procedural "cic:/CoRN/model/structures/Nsec/S_O.con" as lemma.
(*#* ***Apartness
*)
-inline procedural "cic:/CoRN/model/structures/Nsec/ap_nat.con".
+inline procedural "cic:/CoRN/model/structures/Nsec/ap_nat.con" as definition.
(* NOTATION
Infix "{#N}" := ap_nat (no associativity, at level 90).
*)
-inline procedural "cic:/CoRN/model/structures/Nsec/ap_nat_irreflexive0.con".
+inline procedural "cic:/CoRN/model/structures/Nsec/ap_nat_irreflexive0.con" as lemma.
-inline procedural "cic:/CoRN/model/structures/Nsec/ap_nat_symmetric0.con".
+inline procedural "cic:/CoRN/model/structures/Nsec/ap_nat_symmetric0.con" as lemma.
-inline procedural "cic:/CoRN/model/structures/Nsec/ap_nat_cotransitive0.con".
+inline procedural "cic:/CoRN/model/structures/Nsec/ap_nat_cotransitive0.con" as lemma.
-inline procedural "cic:/CoRN/model/structures/Nsec/ap_nat_tight0.con".
+inline procedural "cic:/CoRN/model/structures/Nsec/ap_nat_tight0.con" as lemma.
(*#* ***Addition
*)
-inline procedural "cic:/CoRN/model/structures/Nsec/plus_strext0.con".
+inline procedural "cic:/CoRN/model/structures/Nsec/plus_strext0.con" as lemma.
(*#* There is no inverse for addition, because every candidate will fail for 2
*)
-inline procedural "cic:/CoRN/model/structures/Nsec/no_inverse0.con".
+inline procedural "cic:/CoRN/model/structures/Nsec/no_inverse0.con" as lemma.
(*#* ***Multiplication
*)
-inline procedural "cic:/CoRN/model/structures/Nsec/mult_strext0.con".
+inline procedural "cic:/CoRN/model/structures/Nsec/mult_strext0.con" as lemma.