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 *)
-
-(*#**********************************************************************)
-
include "Num/LtProps.ma".
include "Num/LeAxioms.ma".
-(*#* Properties of the relation [<=] *)
+(* UNAVAILABLE OBJECT: cic:/Coq/Num/LeProps/lt_le.con *********************)
inline procedural "cic:/Coq/Num/LeProps/lt_le.con" as lemma.
+(* UNAVAILABLE OBJECT: cic:/Coq/Num/LeProps/eq_le.con *********************)
+
inline procedural "cic:/Coq/Num/LeProps/eq_le.con" as lemma.
-(*#* compatibility with equality *)
+(* UNAVAILABLE OBJECT: cic:/Coq/Num/LeProps/le_eq_compat.con **************)
inline procedural "cic:/Coq/Num/LeProps/le_eq_compat.con" as lemma.
-(* UNEXPORTED
-Hints Resolve le_eq_compat : num.
-*)
-
-(*#* Transitivity *)
+(* UNAVAILABLE OBJECT: cic:/Coq/Num/LeProps/le_trans.con ******************)
inline procedural "cic:/Coq/Num/LeProps/le_trans.con" as lemma.
-(* UNEXPORTED
-Hints Resolve le_trans : num.
-*)
-
-(*#* compatibility with equality, addition and successor *)
+(* UNAVAILABLE OBJECT: cic:/Coq/Num/LeProps/le_add_compat_l.con ***********)
inline procedural "cic:/Coq/Num/LeProps/le_add_compat_l.con" as lemma.
-(* UNEXPORTED
-Hints Resolve le_add_compat_l : num.
-*)
+(* UNAVAILABLE OBJECT: cic:/Coq/Num/LeProps/le_add_compat_r.con ***********)
inline procedural "cic:/Coq/Num/LeProps/le_add_compat_r.con" as lemma.
-(* UNEXPORTED
-Hints Resolve le_add_compat_r : num.
-*)
+(* UNAVAILABLE OBJECT: cic:/Coq/Num/LeProps/le_add_compat.con *************)
inline procedural "cic:/Coq/Num/LeProps/le_add_compat.con" as lemma.
-(* UNEXPORTED
-Hints Immediate le_add_compat : num.
-*)
-
-(* compatibility with successor *)
+(* UNAVAILABLE OBJECT: cic:/Coq/Num/LeProps/le_S_compat.con ***************)
inline procedural "cic:/Coq/Num/LeProps/le_S_compat.con" as lemma.
-(* UNEXPORTED
-Hints Resolve le_S_compat : num.
-*)
-
-(*#* relating [<=] with [<] *)
+(* UNAVAILABLE OBJECT: cic:/Coq/Num/LeProps/le_lt_x_Sy.con ****************)
inline procedural "cic:/Coq/Num/LeProps/le_lt_x_Sy.con" as lemma.
-(* UNEXPORTED
-Hints Immediate le_lt_x_Sy : num.
-*)
+(* UNAVAILABLE OBJECT: cic:/Coq/Num/LeProps/le_le_x_Sy.con ****************)
inline procedural "cic:/Coq/Num/LeProps/le_le_x_Sy.con" as lemma.
-(* UNEXPORTED
-Hints Immediate le_le_x_Sy : num.
-*)
+(* UNAVAILABLE OBJECT: cic:/Coq/Num/LeProps/le_Sx_y_lt.con ****************)
inline procedural "cic:/Coq/Num/LeProps/le_Sx_y_lt.con" as lemma.
-(* UNEXPORTED
-Hints Immediate le_Sx_y_lt : num.
-*)
-
-(*#* Combined transitivity *)
+(* UNAVAILABLE OBJECT: cic:/Coq/Num/LeProps/lt_le_trans.con ***************)
inline procedural "cic:/Coq/Num/LeProps/lt_le_trans.con" as lemma.
-inline procedural "cic:/Coq/Num/LeProps/le_lt_trans.con" as lemma.
+(* UNAVAILABLE OBJECT: cic:/Coq/Num/LeProps/le_lt_trans.con ***************)
-(* UNEXPORTED
-Hints Immediate lt_le_trans le_lt_trans : num.
-*)
+inline procedural "cic:/Coq/Num/LeProps/le_lt_trans.con" as lemma.
-(*#* weaker compatibility results involving [<] and [<=] *)
+(* UNAVAILABLE OBJECT: cic:/Coq/Num/LeProps/lt_add_compat_weak_l.con ******)
inline procedural "cic:/Coq/Num/LeProps/lt_add_compat_weak_l.con" as lemma.
-(* UNEXPORTED
-Hints Immediate lt_add_compat_weak_l : num.
-*)
+(* UNAVAILABLE OBJECT: cic:/Coq/Num/LeProps/lt_add_compat_weak_r.con ******)
inline procedural "cic:/Coq/Num/LeProps/lt_add_compat_weak_r.con" as lemma.
-(* UNEXPORTED
-Hints Immediate lt_add_compat_weak_r : num.
-*)
-