set "baseuri" "cic:/matita/CoRN-Decl/algebra/COrdAbs".
-include "CoRN_notation.ma".
+include "CoRN.ma".
include "algebra/COrdFields2.ma".
(* begin hide *)
+(* NOTATION
+Notation ZeroR := (Zero:R).
+*)
+
(* end hide *)
inline "cic:/CoRN/algebra/COrdAbs/AbsSmall_leEq_trans.con".
inline "cic:/CoRN/algebra/COrdAbs/absBig.con".
+(* NOTATION
+Notation AbsBig := (absBig _).
+*)
+
inline "cic:/CoRN/algebra/COrdAbs/AbsBigSmall_minus.con".
(* UNEXPORTED