inline "cic:/CoRN/algebra/COrdFields/COrdField.ind".
-coercion "cic:/matita/CoRN-Decl/algebra/COrdFields/cof_crr.con" 0 (* compounds *).
+coercion cic:/matita/CoRN-Decl/algebra/COrdFields/cof_crr.con 0 (* compounds *).
(*#*
%\begin{nameconvention}%
Implicit Arguments cof_less [c].
*)
+(* NOTATION
+Infix "[<]" := cof_less (at level 70, no associativity).
+*)
+
inline "cic:/CoRN/algebra/COrdFields/greater.con".
(* UNEXPORTED
Implicit Arguments greater [F].
*)
+(* NOTATION
+Infix "[>]" := greater (at level 70, no associativity).
+*)
+
(* End_SpecReals *)
(*#*
Implicit Arguments leEq [F].
*)
+(* NOTATION
+Infix "[<=]" := leEq (at level 70, no associativity).
+*)
+
(* UNEXPORTED
Section COrdField_axioms.
*)
Declare Right Step leEq_wdr.
*)
+(* NOTATION
+Notation " x [/]OneNZ" := (x[/] One[//]ring_non_triv _) (at level 20).
+*)
+
+(* NOTATION
+Notation " x [/]TwoNZ" := (x[/] Two[//]two_ap_zero _) (at level 20).
+*)
+
+(* NOTATION
+Notation " x [/]ThreeNZ" := (x[/] Three[//]three_ap_zero _) (at level 20).
+*)
+
+(* NOTATION
+Notation " x [/]FourNZ" := (x[/] Four[//]four_ap_zero _) (at level 20).
+*)
+
+(* NOTATION
+Notation " x [/]SixNZ" := (x[/] Six[//]six_ap_zero _) (at level 20).
+*)
+
+(* NOTATION
+Notation " x [/]EightNZ" := (x[/] Eight[//]eight_ap_zero _) (at level 20).
+*)
+
+(* NOTATION
+Notation " x [/]NineNZ" := (x[/] Nine[//]nine_ap_zero _) (at level 20).
+*)
+
+(* NOTATION
+Notation " x [/]TwelveNZ" := (x[/] Twelve[//]twelve_ap_zero _) (at level 20).
+*)
+
+(* NOTATION
+Notation " x [/]SixteenNZ" := (x[/] Sixteen[//]sixteen_ap_zero _) (at level 20).
+*)
+
+(* NOTATION
+Notation " x [/]EighteenNZ" := (x[/] Eighteen[//]eighteen_ap_zero _) (at level 20).
+*)
+
+(* NOTATION
+Notation " x [/]TwentyFourNZ" := (x[/] TwentyFour[//]twentyfour_ap_zero _) (at level 20).
+*)
+
+(* NOTATION
+Notation " x [/]FortyEightNZ" := (x[/] FortyEight[//]fortyeight_ap_zero _) (at level 20).
+*)
+
(* UNEXPORTED
Section consequences_of_infinity.
*)