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: DiscrProps.v,v 1.4 2002/04/17 11:30:20 herbelin Exp $ i*)
-
include "Num/DiscrAxioms.ma".
include "Num/LtProps.ma".
-(*#* Properties of a discrete order *)
+(* UNAVAILABLE OBJECT: cic:/Coq/Num/DiscrProps/lt_le_Sx_y.con *************)
inline procedural "cic:/Coq/Num/DiscrProps/lt_le_Sx_y.con" as lemma.
-(* UNEXPORTED
-Hints Resolve lt_le_Sx_y : num.
-*)
-