From: Andrea Asperti 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.