A few extensions for the moebius inversion theorem

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

diff --git a/matita/library/nat/primes.ma b/matita/library/nat/primes.ma
index 4298eb9425f11914cdf6f036d310285d0baea6ec..d2e89b8f1b56de4e2de72fc7673f008d909e01cf 100644 (file)
--- 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.