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.
+Section COrdField_axioms
*)
(*#*
%\end{convention}%
*)
-inline "cic:/CoRN/algebra/COrdFields/F.var".
+alias id "F" = "cic:/CoRN/algebra/COrdFields/COrdField_axioms/F.var".
inline "cic:/CoRN/algebra/COrdFields/COrdField_is_COrdField.con".
inline "cic:/CoRN/algebra/COrdFields/less_wdl.con".
(* UNEXPORTED
-End COrdField_axioms.
+End COrdField_axioms
*)
(* UNEXPORTED
*)
(* UNEXPORTED
-Section OrdField_basics.
+Section OrdField_basics
*)
(*#*
%\end{convention}%
*)
-inline "cic:/CoRN/algebra/COrdFields/R.var".
+alias id "R" = "cic:/CoRN/algebra/COrdFields/OrdField_basics/R.var".
inline "cic:/CoRN/algebra/COrdFields/less_imp_ap.con".
inline "cic:/CoRN/algebra/COrdFields/leEq_not_eq.con".
(* UNEXPORTED
-End OrdField_basics.
+End OrdField_basics
*)
(*#**********************************)
(* UNEXPORTED
-Section Basic_Properties_of_leEq.
+Section Basic_Properties_of_leEq
*)
(*#**********************************)
(*#* ** Basic properties of [ [<=] ]
*)
-inline "cic:/CoRN/algebra/COrdFields/R.var".
+alias id "R" = "cic:/CoRN/algebra/COrdFields/Basic_Properties_of_leEq/R.var".
inline "cic:/CoRN/algebra/COrdFields/leEq_wdr.con".
inline "cic:/CoRN/algebra/COrdFields/less_leEq.con".
(* UNEXPORTED
-End Basic_Properties_of_leEq.
+End Basic_Properties_of_leEq
*)
(* UNEXPORTED
*)
(* UNEXPORTED
-Section infinity_of_cordfields.
+Section infinity_of_cordfields
*)
(*#*
e.g.%\% [x[/]TwoNZ].
*)
-inline "cic:/CoRN/algebra/COrdFields/R.var".
+alias id "R" = "cic:/CoRN/algebra/COrdFields/infinity_of_cordfields/R.var".
inline "cic:/CoRN/algebra/COrdFields/pos_one.con".
include "tactics/Opaque_algebra.ma".
(* UNEXPORTED
-Section up_to_four.
+Section up_to_four
*)
(*#*
inline "cic:/CoRN/algebra/COrdFields/four_ap_zero.con".
(* UNEXPORTED
-End up_to_four.
+End up_to_four
*)
(* UNEXPORTED
-Section More_than_four.
+Section More_than_four
*)
(*#* *** Properties of some other numbers *)
inline "cic:/CoRN/algebra/COrdFields/fortyeight_ap_zero.con".
(* UNEXPORTED
-End More_than_four.
+End More_than_four
*)
(* UNEXPORTED
-End infinity_of_cordfields.
+End infinity_of_cordfields
*)
(* UNEXPORTED
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.
+Section consequences_of_infinity
*)
(*#*
*** Consequences of infinity
*)
-inline "cic:/CoRN/algebra/COrdFields/F.var".
+alias id "F" = "cic:/CoRN/algebra/COrdFields/consequences_of_infinity/F.var".
inline "cic:/CoRN/algebra/COrdFields/square_eq.con".
inline "cic:/CoRN/algebra/COrdFields/char0_OrdField.con".
(* UNEXPORTED
-End consequences_of_infinity.
+End consequences_of_infinity
*)
(*#**********************************)
(* UNEXPORTED
-Section Properties_of_Ordering.
+Section Properties_of_Ordering
*)
(*#**********************************)
** Properties of [[<]]
*)
-inline "cic:/CoRN/algebra/COrdFields/R.var".
+alias id "R" = "cic:/CoRN/algebra/COrdFields/Properties_of_Ordering/R.var".
(*#*
We do not use a special predicate for positivity,
*)
(* UNEXPORTED
-Section addition.
+Section addition
*)
(*#*
inline "cic:/CoRN/algebra/COrdFields/qltone.con".
(* UNEXPORTED
-End addition.
+End addition
*)
(* UNEXPORTED
-Section multiplication.
+Section multiplication
*)
(*#*
inline "cic:/CoRN/algebra/COrdFields/pos_div_fortyeight.con".
(* UNEXPORTED
-End multiplication.
+End multiplication
*)
(* UNEXPORTED
-Section misc.
+Section misc
*)
(*#*
inline "cic:/CoRN/algebra/COrdFields/negative_Sumx.con".
(* UNEXPORTED
-End misc.
+End misc
*)
(* UNEXPORTED
-End Properties_of_Ordering.
+End Properties_of_Ordering
*)