set "baseuri" "cic:/matita/CoRN-Decl/algebra/COrdFields2".
-include "CoRN_notation.ma".
+include "CoRN.ma".
include "algebra/COrdFields.ma".
(* begin hide *)
+(* NOTATION
+Notation ZeroR := (Zero:R).
+*)
+
+(* NOTATION
+Notation OneR := (One:R).
+*)
+
(* end hide *)
inline "cic:/CoRN/algebra/COrdFields2/mult_pos_imp.con".