(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/nat/orders".
-
include "nat/nat.ma".
include "higher_order_defs/ordering.ma".
[ simplify;
apply le_O_n
| simplify;
- generalize in match H1;
- clear H1;
- elim m;
+ elim m in H1 ⊢ %;
[ elim (not_le_Sn_O ? H1)
| simplify;
apply le_S_S_to_le;