From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Wed, 15 Nov 2006 09:06:10 +0000 (+0000)
Subject: Added lt_O_S.
X-Git-Tag: 0.4.95@7852~810
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=57e4568829db52f1959006041d72036ae9663955;p=helm.git

Added lt_O_S.
---

diff --git a/matita/library/nat/orders.ma b/matita/library/nat/orders.ma
index 312487055..587134afc 100644
--- a/matita/library/nat/orders.ma
+++ b/matita/library/nat/orders.ma
@@ -192,6 +192,10 @@ apply H3. apply le_S_S. 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.