X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Fnat%2Forders.ma;h=42454393ca45cc08676ef8205d878a437a1266f2;hb=683978a2627cf1ce15673360f26806593d22f7b5;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..42454393c 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.
@@ -139,6 +145,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.
@@ -182,8 +201,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.
@@ -201,7 +220,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