X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Flibrary%2Fnat%2Forders.ma;h=8053d50de55bfe8afc7d434243b17ceca34b9536;hb=6ff5322f46c2e88e07b4c345bc45edda7042128a;hp=6ec0c9992a68b18e15976e96e74ef853c2fc04eb;hpb=7f2444c2670cadafddd8785b687ef312158376b0;p=helm.git

diff --git a/matita/library/nat/orders.ma b/matita/library/nat/orders.ma
index 6ec0c9992..8053d50de 100644
--- a/matita/library/nat/orders.ma
+++ b/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.
@@ -129,6 +139,19 @@ apply Hcut.assumption.rewrite < H1.
 apply not_le_Sn_n.
 qed.
 
+(*not lt*)
+theorem eq_to_not_lt: \forall a,b:nat.
+a = b \to a \nlt b.
+intros.
+unfold Not.
+intros.
+rewrite > H in H1.
+apply (lt_to_not_eq b b)
+[ assumption
+| reflexivity
+]
+qed.
+
 (* le vs. lt *)
 theorem lt_to_le : \forall n,m:nat. n<m \to n \leq m.
 simplify.intros.unfold lt in H.elim H.
@@ -163,8 +186,7 @@ apply not_le_to_lt.exact H.
 qed.
 
 theorem le_to_not_lt: \forall n,m:nat. le n m \to Not (lt m n).
-intros.
-change with (Not (le (S m) n)).
+intros.unfold Not.unfold lt.
 apply lt_to_not_le.unfold lt.
 apply le_S_S.assumption.
 qed.
@@ -173,8 +195,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.
@@ -192,7 +214,23 @@ apply H2.reflexivity.
 apply H3. apply le_S_S. assumption.
 qed.
 
+(* 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
+  |intros.apply sym_eq.apply le_n_O_to_eq.assumption
+  |intros.apply eq_f.apply H
+    [apply le_S_S_to_le.assumption
+    |apply le_S_S_to_le.assumption
+    ]
+  ]
+qed.
+
 (* lt and le trans *)
+theorem lt_O_S : \forall n:nat. O < S n.
+intro. unfold. apply le_S_S. apply le_O_n.
+qed.
+
 theorem lt_to_le_to_lt: \forall n,m,p:nat. lt n m \to le m p \to lt n p.
 intros.elim H1.
 assumption.unfold lt.apply le_S.assumption.
@@ -204,6 +242,12 @@ assumption.apply H2.unfold lt.
 apply lt_to_le.assumption.
 qed.
 
+theorem lt_S_to_lt: \forall n,m. S n < m \to n < m.
+intros.
+apply (trans_lt ? (S n))
+  [apply le_n|assumption]
+qed.
+
 theorem ltn_to_ltO: \forall n,m:nat. lt n m \to lt O m.
 intros.apply (le_to_lt_to_lt O n).
 apply le_O_n.assumption.