X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Fnat%2Fprimes.ma;h=d2e89b8f1b56de4e2de72fc7673f008d909e01cf;hb=6e61c5884aa89838a04659f90dc8d210e3703502;hp=4298eb9425f11914cdf6f036d310285d0baea6ec;hpb=6423f1b6e3056883016598e454c55cab1004dfd2;p=helm.git

diff --git a/helm/software/matita/library/nat/primes.ma b/helm/software/matita/library/nat/primes.ma
index 4298eb942..d2e89b8f1 100644
--- a/helm/software/matita/library/nat/primes.ma
+++ b/helm/software/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.