include "Coq.ma".
-(*#**********************************************************************)
-
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-
-(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
-
-(* \VV/ *************************************************************)
-
-(* // * This file is distributed under the terms of the *)
-
-(* * GNU Lesser General Public License Version 2.1 *)
-
-(*#**********************************************************************)
-
-(*i $Id: GeAxioms.v,v 1.3 2002/02/14 14:39:02 filliatr Exp $ i*)
-
include "Num/Axioms.ma".
include "Num/LtProps.ma".
-(*#* Axiomatizing [>=] from [<] *)
+(* UNAVAILABLE OBJECT: cic:/Coq/Num/GeAxioms/not_lt_ge.con ****************)
inline procedural "cic:/Coq/Num/GeAxioms/not_lt_ge.con".
-inline procedural "cic:/Coq/Num/GeAxioms/ge_not_lt.con".
+(* UNAVAILABLE OBJECT: cic:/Coq/Num/GeAxioms/ge_not_lt.con ****************)
-(* UNEXPORTED
-Hints Resolve not_lt_ge : num.
-*)
-
-(* UNEXPORTED
-Hints Immediate ge_not_lt : num.
-*)
+inline procedural "cic:/Coq/Num/GeAxioms/ge_not_lt.con".