X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=matita%2Flibrary%2Fnat%2Forders.ma;h=42454393ca45cc08676ef8205d878a437a1266f2;hb=80f85c7fb53791fd72c0e64450c3c87d8f30b84d;hp=8053d50de55bfe8afc7d434243b17ceca34b9536;hpb=77440acc493b0e04b7e009b942c6a3268a46c141;p=helm.git

diff --git a/matita/library/nat/orders.ma b/matita/library/nat/orders.ma
index 8053d50de..42454393c 100644
--- a/matita/library/nat/orders.ma
+++ b/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.