X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Fnat%2Forders.ma;h=799f8bf7c47b74c65575431e78d2f0b8f9662b9e;hb=10f29fdd78ee089a9a94446207b543d33d6c851c;hp=8c6ce942e33b0d272a8cadbbaabbc48e93eb6e49;hpb=f275a4daa42f8ab455020ec5a7ce7bf69b460c37;p=helm.git

diff --git a/helm/software/matita/library/nat/orders.ma b/helm/software/matita/library/nat/orders.ma
index 8c6ce942e..799f8bf7c 100644
--- a/helm/software/matita/library/nat/orders.ma
+++ b/helm/software/matita/library/nat/orders.ma
@@ -100,6 +100,12 @@ theorem lt_S_S_to_lt: \forall n,m.
 intros. apply le_S_S_to_le. assumption.
 qed.
 
+theorem lt_to_lt_S_S: ∀n,m. n < m → S n < S m.
+intros;
+unfold lt in H;
+apply (le_S_S ? ? H).
+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.
@@ -124,6 +130,43 @@ apply nat_elim2
   ]
 qed.
 
+theorem S_pred: \forall n:nat.lt O n \to eq nat n (S (pred n)).
+intro.elim n.apply False_ind.exact (not_le_Sn_O O H).
+apply eq_f.apply pred_Sn.
+qed.
+
+theorem le_pred_to_le:
+ ∀n,m. O < m → pred n ≤ pred m → n ≤ m.
+intros 2;
+elim n;
+[ apply le_O_n
+| simplify in H2;
+  rewrite > (S_pred m);
+  [ apply le_S_S;
+    assumption
+  | assumption
+  ]
+].
+qed.
+
+theorem le_to_le_pred:
+ ∀n,m. n ≤ m → pred n ≤ pred m.
+intros 2;
+elim n;
+[ simplify;
+  apply le_O_n
+| simplify;
+  generalize in match H1;
+  clear H1;
+  elim m;
+  [ elim (not_le_Sn_O ? H1)
+  | simplify;
+    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.
@@ -132,6 +175,14 @@ right.reflexivity.
 left.unfold lt.apply le_S_S.assumption.
 qed.
 
+theorem Not_lt_n_n: ∀n. n ≮ n.
+intro;
+unfold Not;
+intro;
+unfold lt in H;
+apply (not_le_Sn_n ? H).
+qed.
+
 (* not eq *)
 theorem lt_to_not_eq : \forall n,m:nat. n<m \to n \neq m.
 unfold Not.intros.cut ((le (S n) m) \to False).
@@ -139,6 +190,32 @@ 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.
+
+theorem lt_n_m_to_not_lt_m_Sn: ∀n,m. n < m → m ≮ S n.
+intros;
+unfold Not;
+intro;
+unfold lt in H;
+unfold lt in H1;
+generalize in match (le_S_S ? ? H);
+intro;
+generalize in match (transitive_le ? ? ? H2 H1);
+intro;
+apply (not_le_Sn_n ? H3).
+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.
@@ -178,12 +255,20 @@ apply lt_to_not_le.unfold lt.
 apply le_S_S.assumption.
 qed.
 
+theorem not_eq_to_le_to_lt: ∀n,m. n≠m → n≤m → n<m.
+intros;
+elim (le_to_or_lt_eq ? ? H1);
+[ assumption
+| elim (H H2)
+].
+qed.
+
 (* le elimination *)
 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.
@@ -201,7 +286,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
@@ -240,6 +325,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).
@@ -260,6 +355,15 @@ qed.
 theorem antisym_le: \forall n,m:nat. n \leq m \to m \leq n \to n=m
 \def antisymmetric_le.
 
+theorem le_n_m_to_lt_m_Sn_to_eq_n_m: ∀n,m. n ≤ m → m < S n → n=m.
+intros;
+unfold lt in H1;
+generalize in match (le_S_S_to_le ? ? H1);
+intro;
+apply antisym_le;
+assumption.
+qed.
+
 theorem decidable_le: \forall n,m:nat. decidable (n \leq m).
 intros.
 apply (nat_elim2 (\lambda n,m.decidable (n \leq m))).