Even more Q stuff classified.

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

diff --git a/helm/software/matita/library/nat/sieve.ma b/helm/software/matita/library/nat/sieve.ma
index 6b428d578c1131b716086dc0c66a8a9952970717..3525bc0b2280c92b19c7223836384714b70679aa 100644 (file)
--- a/helm/software/matita/library/nat/sieve.ma
+++ b/helm/software/matita/library/nat/sieve.ma
@@ -12,9 +12,8 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "nat/sqrt.ma".
+include "nat/primes.ma".
 include "list/sort.ma".
-include "nat/factorization.ma".
 
 let rec list_n_aux n k \def
     match n with
@@ -78,21 +77,35 @@ intro.elim t 0
                           [elim H11;assumption
                           |apply in_list_head]
                        |intros;elim (le_to_or_lt_eq ? ? (divides_to_le ? ? ? H9))
-                          [elim (divides_to_prime_divides ? ? H10 H11 H9);elim H12;
-                           elim H13;clear H13 H12;elim (H3 a);elim H12
-                             [clear H13 H12;elim (H18 ? ? H14);elim (H2 a1);
-                              apply H13
-                                [assumption
-                                |elim H17;apply (trans_le ? ? ? ? H20);
-                                 apply (trans_le ? ? ? H15);
-                                 apply lt_to_le;assumption
-                                |intros;apply (trans_le ? (S m))
-                                   [apply le_S_S;assumption
-                                   |apply (trans_le ? ? ? H11);
-                                    elim (in_list_cons_case ? ? ? ? H19)
-                                      [rewrite > H20;apply le_n
-                                      |apply lt_to_le;apply (sorted_to_minimum ? ? ? ? H6);assumption]]]
-                             |apply in_list_head]
+                          [cut (1 < a) as Lt1a; [2: apply (trans_lt ??? H10 H11)]
+                           letin a1 ≝ (smallest_factor a);
+                           lapply (divides_smallest_factor_n a) as H14;
+                            [2: apply (trans_lt ? (S O) ? ? Lt1a);
+                                apply lt_O_S
+                            | fold unfold a1 a1 in H14;
+                              lapply (prime_smallest_factor_n a Lt1a) as H16;
+                              fold unfold a1 a1 in H16;
+                              cut (a1 ≤ m) as H15;
+                              [2: generalize in match (leb_to_Prop a1 m);
+                                  elim (leb a1 m); simplify in H12;
+                                   [ assumption
+                                   | elim (lt_smallest_factor_to_not_divides a m Lt1a H10 ? H9);
+                                     apply (not_le_to_lt ?? H12)]
+                              | clearbody a1;
+                                elim (H3 a);elim H12
+                                [clear H13 H12;elim (H18 ? ? H14);elim (H2 a1);
+                                 apply H13
+                                   [assumption
+                                   |elim H17;apply (trans_le ? ? ? ? H20);
+                                    apply (trans_le ? ? ? H15);
+                                    apply lt_to_le;assumption
+                                   |intros;apply (trans_le ? (S m))
+                                      [apply le_S_S;assumption
+                                      |apply (trans_le ? ? ? H11);
+                                       elim (in_list_cons_case ? ? ? ? H19)
+                                         [rewrite > H20;apply le_n
+                                         |apply lt_to_le;apply (sorted_to_minimum ? ? ? ? H6);assumption]]]
+                                |apply in_list_head]]]
                           |elim (H3 a);elim H11
                              [elim H13;apply lt_to_le;assumption
                              |apply in_list_head]