From 57e4568829db52f1959006041d72036ae9663955 Mon Sep 17 00:00:00 2001
From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Wed, 15 Nov 2006 09:06:10 +0000
Subject: [PATCH] Added lt_O_S.

---
 matita/library/nat/orders.ma | 4 ++++
 1 file changed, 4 insertions(+)

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.
-- 
2.39.2