X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=matita%2Flibrary%2Fnat%2Fprimes.ma;h=d2e89b8f1b56de4e2de72fc7673f008d909e01cf;hb=72e7d9c9d410ded571b9d3c396197b26181c1e2a;hp=4298eb9425f11914cdf6f036d310285d0baea6ec;hpb=e95f5d784fe7830fe9ed10b3e782ef2206fea896;p=helm.git

diff --git a/matita/library/nat/primes.ma b/matita/library/nat/primes.ma
index 4298eb942..d2e89b8f1 100644
--- a/matita/library/nat/primes.ma
+++ b/matita/library/nat/primes.ma
@@ -385,6 +385,10 @@ theorem not_prime_SO: \lnot (prime (S O)).
 unfold Not.unfold prime.intro.elim H.apply (not_le_Sn_n (S O) H1).
 qed.
 
+theorem prime_to_lt_O: \forall p. prime p \to O < p.
+intros.elim H.apply lt_to_le.assumption.
+qed.
+
 (* smallest factor *)
 definition smallest_factor : nat \to nat \def
 \lambda n:nat.