X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Fnat%2Forders.ma;h=3257e2e1a623d1f348f9d149bba0a0c7478355e2;hb=cf4088e2cabcbce9b112f1e1fd5cfd38fe16d427;hp=807906bd21abd4572f75e96fa9bd39977a2309e5;hpb=f79585fe2f19c4a545938e189439d87b2611a47a;p=helm.git

diff --git a/helm/software/matita/library/nat/orders.ma b/helm/software/matita/library/nat/orders.ma
index 807906bd2..3257e2e1a 100644
--- a/helm/software/matita/library/nat/orders.ma
+++ b/helm/software/matita/library/nat/orders.ma
@@ -22,9 +22,8 @@ inductive le (n:nat) : nat \to Prop \def
   | le_n : le n n
   | le_S : \forall m:nat. le n m \to le n (S m).
 
-(*CSC: the URI must disappear: there is a bug now *)
 interpretation "natural 'less or equal to'" 'leq x y = (cic:/matita/nat/orders/le.ind#xpointer(1/1) x y).
-(*CSC: the URI must disappear: there is a bug now *)
+
 interpretation "natural 'neither less nor equal to'" 'nleq x y =
   (cic:/matita/logic/connectives/Not.con
     (cic:/matita/nat/orders/le.ind#xpointer(1/1) x y)).
@@ -32,24 +31,21 @@ interpretation "natural 'neither less nor equal to'" 'nleq x y =
 definition lt: nat \to nat \to Prop \def
 \lambda n,m:nat.(S n) \leq m.
 
-(*CSC: the URI must disappear: there is a bug now *)
 interpretation "natural 'less than'" 'lt x y = (cic:/matita/nat/orders/lt.con x y).
-(*CSC: the URI must disappear: there is a bug now *)
+
 interpretation "natural 'not less than'" 'nless x y =
   (cic:/matita/logic/connectives/Not.con (cic:/matita/nat/orders/lt.con x y)).
 
 definition ge: nat \to nat \to Prop \def
 \lambda n,m:nat.m \leq n.
 
-(*CSC: the URI must disappear: there is a bug now *)
 interpretation "natural 'greater or equal to'" 'geq x y = (cic:/matita/nat/orders/ge.con x y).
 
 definition gt: nat \to nat \to Prop \def
 \lambda n,m:nat.m<n.
 
-(*CSC: the URI must disappear: there is a bug now *)
 interpretation "natural 'greater than'" 'gt x y = (cic:/matita/nat/orders/gt.con x y).
-(*CSC: the URI must disappear: there is a bug now *)
+
 interpretation "natural 'not greater than'" 'ngtr x y =
   (cic:/matita/logic/connectives/Not.con (cic:/matita/nat/orders/gt.con x y)).
 
@@ -99,6 +95,11 @@ elim H.apply le_n.apply (trans_le ? (pred n1)).assumption.
 apply le_pred_n.
 qed.
 
+theorem lt_S_S_to_lt: \forall n,m. 
+  S n < S m \to n < m.
+intros. apply le_S_S_to_le. assumption.
+qed.
+
 theorem leS_to_not_zero : \forall n,m:nat. S n \leq m \to not_zero m.
 intros.elim H.exact I.exact I.
 qed.
@@ -114,6 +115,15 @@ apply H.assumption.
 apply le_S_S_to_le.assumption.
 qed.
 
+theorem lt_pred: \forall n,m. 
+  O < n \to n < m \to pred n < pred m. 
+apply nat_elim2
+  [intros.apply False_ind.apply (not_le_Sn_O ? H)
+  |intros.apply False_ind.apply (not_le_Sn_O ? H1)
+  |intros.simplify.unfold.apply le_S_S_to_le.assumption
+  ]
+qed.
+
 (* le to lt or eq *)
 theorem le_to_or_lt_eq : \forall n,m:nat. 
 n \leq m \to n < m \lor n = m.
@@ -172,8 +182,8 @@ qed.
 theorem le_n_O_to_eq : \forall n:nat. n \leq O \to O=n.
 intro.elim n.reflexivity.
 apply False_ind.
-apply not_le_Sn_O.
-goal 17. apply H1.
+apply not_le_Sn_O;
+[2: apply H1 | skip].
 qed.
 
 theorem le_n_O_elim: \forall n:nat.n \leq O \to \forall P: nat \to Prop.
@@ -191,7 +201,7 @@ apply H2.reflexivity.
 apply H3. apply le_S_S. assumption.
 qed.
 
-(* le to eq *)
+(* le and eq *)
 lemma le_to_le_to_eq: \forall n,m. n \le m \to m \le n \to n = m.
 apply nat_elim2
   [intros.apply le_n_O_to_eq.assumption