Even more Q stuff classified.

[helm.git] / helm / software / matita / library / nat / factorization.ma

diff --git a/helm/software/matita/library/nat/factorization.ma b/helm/software/matita/library/nat/factorization.ma
index 8c50d1d7db1e5612e160776b39a59e55ab21fece..d649fbe145a4022e3f6a34115b87f9fae1f4ef9c 100644 (file)
--- a/helm/software/matita/library/nat/factorization.ma
+++ b/helm/software/matita/library/nat/factorization.ma
@@ -12,8 +12,6 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/nat/factorization".
-
 include "nat/ord.ma".
 
 (* the following factorization algorithm looks for the largest prime
@@ -63,7 +61,7 @@ cut (\exists i. nth_prime i = smallest_factor n);
       [ apply (trans_lt ? (S O));
         [ unfold lt; apply le_n;
         | apply lt_SO_smallest_factor; assumption; ]
-      | letin x \def le.autobatch new.
+      | letin x \def le.autobatch.
          (*       
        apply divides_smallest_factor_n;
         apply (trans_lt ? (S O));
@@ -76,6 +74,18 @@ cut (\exists i. nth_prime i = smallest_factor n);
     assumption; *) ] 
 qed.
 
+lemma divides_to_prime_divides : \forall n,m.1 < m \to m < n \to m \divides n \to
+ \exists p.p \leq m \land prime p \land p \divides n.
+intros;apply (ex_intro ? ? (nth_prime (max_prime_factor m)));split
+  [split
+     [apply divides_to_le
+        [apply lt_to_le;assumption
+        |apply divides_max_prime_factor_n;assumption]
+     |apply prime_nth_prime;]
+  |apply (transitive_divides ? ? ? ? H2);apply divides_max_prime_factor_n;
+   assumption]
+qed.
+
 theorem divides_to_max_prime_factor : \forall n,m. (S O) < n \to O < m \to n \divides m \to 
 max_prime_factor n \le max_prime_factor m.
 intros.unfold max_prime_factor.
@@ -146,7 +156,7 @@ apply divides_max_prime_factor_n.
 assumption.unfold Not.
 intro.
 cut (r \mod (nth_prime (max_prime_factor n)) \neq O);
-  [unfold Not in Hcut1.autobatch new.
+  [unfold Not in Hcut1.autobatch.
     (*
     apply Hcut1.apply divides_to_mod_O;
     [ apply lt_O_nth_prime_n.