X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Fnat%2Forders.ma;h=6dd8773f8820062586cacd3df6ebbea26afa8421;hb=c99a38b6539be1eb667cced1eed2db3fc75e3162;hp=caecbe0632eb8bfd2219275403c012e000831743;hpb=af130d273b6be7fbcc2fb2504f3b28ef8fa2344f;p=helm.git

diff --git a/helm/software/matita/library/nat/orders.ma b/helm/software/matita/library/nat/orders.ma
index caecbe063..6dd8773f8 100644
--- a/helm/software/matita/library/nat/orders.ma
+++ b/helm/software/matita/library/nat/orders.ma
@@ -12,8 +12,6 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/nat/orders".
-
 include "nat/nat.ma".
 include "higher_order_defs/ordering.ma".
 
@@ -156,9 +154,7 @@ elim n;
 [ 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;
@@ -325,6 +321,16 @@ intros.apply (le_to_lt_to_lt O n).
 apply le_O_n.assumption.
 qed.
 
+theorem lt_SO_n_to_lt_O_pred_n: \forall n:nat.
+(S O) \lt n \to O \lt (pred n).
+intros.
+apply (ltn_to_ltO (pred (S O)) (pred n) ?).
+ apply (lt_pred (S O) n);
+ [ apply (lt_O_S O) 
+ | assumption
+ ]
+qed.
+
 theorem lt_O_n_elim: \forall n:nat. lt O n \to 
 \forall P:nat\to Prop. (\forall m:nat.P (S m)) \to P n.
 intro.elim n.apply False_ind.exact (not_le_Sn_O O H).