X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Flibrary%2Fnat%2Fprimes.ma;h=d2e89b8f1b56de4e2de72fc7673f008d909e01cf;hb=c3bba4af040f8040e5eae07e70690c52f8c614f8;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.