Added lt_O_S.

[helm.git] / matita / library / nat / orders.ma

diff --git a/matita/library/nat/orders.ma b/matita/library/nat/orders.ma
index 312487055e8f7a9442c3c7ab6050aaa89ab1635d..587134afcc9c0873eea6fa14a61677e34fbb6e63 100644 (file)
--- 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.