X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Fnat%2Fbertrand.ma;h=4d8596b6ebea5b1b22413022a5c78f5ea2f5a3f9;hb=097e94fd9b070378d68dbfe8e7cba18b14ed8518;hp=bb4fde4973ac9e7f1f3e67472c366c81095f0b11;hpb=286b2c5ed05fc545a2ac69af4cd39d1f35a53b68;p=helm.git

diff --git a/helm/software/matita/library/nat/bertrand.ma b/helm/software/matita/library/nat/bertrand.ma
index bb4fde497..4d8596b6e 100644
--- a/helm/software/matita/library/nat/bertrand.ma
+++ b/helm/software/matita/library/nat/bertrand.ma
@@ -15,7 +15,8 @@
 include "nat/sqrt.ma".
 include "nat/chebyshev_teta.ma".
 include "nat/chebyshev.ma".
-include "list/list.ma".
+include "list/in.ma".
+include "list/sort.ma".
 include "nat/o.ma".
 
 let rec list_divides l n \def
@@ -32,18 +33,6 @@ definition lprim : nat \to list nat \def
        | false => aux m1 (n-m1::acc)]]
   in aux (pred n) [].
   
-let rec filter A l p on l \def
-    match l with
-    [ nil => nil A
-    | cons (a:A) (tl:list A) => match (p a) with
-      [ true => a::(filter A tl p)
-      | false => filter A tl p ]].      
-
-let rec length A (l:list A) on l \def
-  match l with
-  [ nil => O
-  | cons (a:A) (tl:list A) => S (length A tl) ].
-
 let rec list_n_aux n k \def
     match n with
     [ O => nil nat
@@ -62,75 +51,6 @@ let rec sieve_aux l1 l2 t on t \def
 definition sieve : nat \to list nat \def
   \lambda m.sieve_aux [] (list_n m) m.
 
-definition ord_list \def
-   \lambda l.
-   \forall a,b,l1,l2.l = l1@(a::b::l2) \to b \leq a.
-   
-definition in_list \def
-   \lambda A.\lambda a:A.\lambda l:list A.
-   \exists l1,l2.l = l1@(a::l2).
-
-lemma in_list_filter_to_p_true : \forall l,x,p.in_list nat x (filter nat l p) \to p x = true.
-intros;elim H;elim H1;clear H H1;generalize in match H2;generalize in match a;elim l 0
-  [simplify;intro;elim l1
-     [simplify in H;destruct H
-     |simplify in H1;destruct H1]
-  |intros;simplify in H1;apply (bool_elim ? (p t));intro;
-   rewrite > H3 in H1;simplify in H1
-     [generalize in match H1;elim l2
-        [simplify in H4;destruct H4;assumption
-        |simplify in H5;destruct H5;apply (H l3);assumption]
-     |apply (H l2);assumption]]
-qed.
-
-lemma in_list_cons : \forall l,x,y.in_list nat x l \to in_list nat x (y::l).
-intros;unfold in H;unfold;elim H;elim H1;apply (ex_intro ? ? (y::a));
-apply (ex_intro ? ? a1);simplify;rewrite < H2;reflexivity.
-qed.
-
-lemma in_list_tail : \forall l,x,y.in_list nat x (y::l) \to x \neq y \to in_list nat x l.
-intros;elim H;elim H2;generalize in match H3;elim a
-  [simplify in H4;destruct H4;elim H1;reflexivity
-  |simplify in H5;destruct H5;apply (ex_intro ? ? l1);apply (ex_intro ? ? a1);
-   reflexivity]
-qed.
-  
-lemma in_list_filter : \forall l,p,x.in_list nat x (filter nat l p) \to in_list nat x l.
-intros;elim H;elim H1;generalize in match H2;generalize in match a;elim l 0
-  [simplify;intro;elim l1
-     [simplify in H3;destruct H3
-     |simplify in H4;destruct H4]
-  |intros;simplify in H4;apply (bool_elim ? (p t));intro
-     [rewrite > H5 in H4;simplify in H4;generalize in match H4;elim l2
-        [simplify in H6;destruct H6;apply (ex_intro ? ? []);apply (ex_intro ? ? l1);
-         simplify;reflexivity
-        |simplify in H7;destruct H7;apply in_list_cons;apply (H3 ? Hcut1);]
-     |rewrite > H5 in H4;simplify in H4;apply in_list_cons;apply (H3 ? H4);]]
-qed.
-
-lemma in_list_filter_r : \forall l,p,x.in_list nat x l \to p x = true \to in_list nat x (filter nat l p).
-intros;elim H;elim H2;rewrite > H3;elim a
-  [simplify;rewrite > H1;simplify;apply (ex_intro ? ? []);apply (ex_intro ? ? (filter nat a1 p));
-   reflexivity
-  |simplify;elim (p t);simplify
-     [apply in_list_cons;assumption
-     |assumption]]
-qed.
-   
-lemma in_list_head : \forall x,l.in_list nat x (x::l).
-intros;apply (ex_intro ? ? []);apply (ex_intro ? ? l);reflexivity;
-qed.
-
-lemma in_list_cons_case : \forall A,x,a,l.in_list A x (a::l) \to
-                          x = a \lor in_list A x l.
-intros;elim H;elim H1;clear H H1;generalize in match H2;elim a1
-  [simplify in H;destruct H;left;reflexivity
-  |simplify in H1;destruct H1;right;
-   apply (ex_intro ? ? l1);
-   apply (ex_intro ? ? a2);
-   reflexivity]
-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
@@ -143,42 +63,8 @@ intros;apply (ex_intro ? ? (nth_prime (max_prime_factor m)));split
    assumption]
 qed.
 
-
-lemma le_length_filter : \forall A,l,p.length A (filter A l p) \leq length A l.
-intros;elim l
-  [simplify;apply le_n
-  |simplify;apply (bool_elim ? (p t));intro
-     [simplify;apply le_S_S;assumption
-     |simplify;apply le_S;assumption]]
-qed.
-
-inductive sorted (P:nat \to nat \to Prop): list nat \to Prop \def
-| sort_nil : sorted P []
-| sort_cons : \forall x,l.sorted P l \to (\forall y.in_list ? y l \to P x y)
-              \to sorted P (x::l).
-              
-definition sorted_lt : list nat \to Prop \def \lambda l.sorted lt l.
-
-definition sorted_gt : list nat \to Prop \def \lambda l.sorted gt l.
-              
-lemma sorted_cons_to_sorted : \forall P,x,l.sorted P (x::l) \to sorted P l.
-intros;inversion H;intros
-  [destruct H1
-  |destruct H4;assumption]
-qed.
-
-lemma sorted_to_minimum : \forall P,x,l.sorted P (x::l) \to 
-                          \forall y.in_list ? y l \to P x y.
-intros;inversion H;intros;
-  [destruct H2
-  |destruct H5;apply H4;assumption]
-qed.
-
-lemma not_in_list_nil : \forall A,a.\lnot in_list A a [].
-intros;intro;elim H;elim H1;generalize in match H2;elim a1
-  [simplify in H3;destruct H3
-  |simplify in H4;destruct H4]
-qed.
+definition sorted_lt \def sorted ? lt.
+definition sorted_gt \def sorted ? gt.
 
 lemma sieve_prime : \forall t,k,l2,l1.
   (\forall p.(in_list ? p l1 \to prime p \land p \leq k \land \forall x.in_list ? x l2 \to p < x) \land
@@ -208,7 +94,7 @@ intro.elim t 0
         |intro;elim (H1 p);split;intros
            [elim (H6 H8);assumption
            |apply (H7 H8 H9);intros;elim (not_in_list_nil ? ? H10)]]
-     |simplify;elim (H k (filter ? l (\lambda x.notb (divides_b t1 x))) (t1::l1))
+     |simplify;elim (H k (filter ? l (\lambda x.notb (divides_b a x))) (a::l1))
         [split;
            [assumption
            |intro;apply H8;]
@@ -217,13 +103,13 @@ intro.elim t 0
               [rewrite > H8;split
                  [split
                     [unfold;intros;split
-                       [elim (H3 t1);elim H9
+                       [elim (H3 a);elim H9
                           [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 t1);elim H12
-                             [clear H13 H12;elim (H18 ? ? H14);elim (H2 a);
+                           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);
@@ -234,70 +120,66 @@ intro.elim t 0
                                    |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]]]
-                             |unfold;apply (ex_intro ? ? []);
-                              apply (ex_intro ? ? l);
-                              reflexivity]
-                          |elim (H3 t1);elim H11
+                                      |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]
                           |assumption]]
-                    |elim (H3 t1);elim H9
+                    |elim (H3 a);elim H9
                        [elim H11;assumption
-                       |apply (ex_intro ? ? []);apply (ex_intro ? ? l);reflexivity]]
-                 |intros;elim (le_to_or_lt_eq t1 x)
+                       |apply in_list_head]]
+                 |intros;elim (le_to_or_lt_eq a x)
                     [assumption
                     |rewrite > H10 in H9;lapply (in_list_filter_to_p_true ? ? ? H9);
                      lapply (divides_n_n x);
                      rewrite > (divides_to_divides_b_true ? ? ? Hletin1) in Hletin
                        [simplify in Hletin;destruct Hletin
-                       |rewrite < H10;elim (H3 t1);elim H11
+                       |rewrite < H10;elim (H3 a);elim H11
                           [elim H13;apply lt_to_le;assumption
                           |apply in_list_head]]
-                    |apply lt_to_le;apply (sorted_to_minimum ? ? ? H6);apply (in_list_filter ? ? ? H9)]]
+                    |apply lt_to_le;apply (sorted_to_minimum ? ? ? ? H6);apply (in_list_filter ? ? ? H9)]]
                  |elim (H2 p);elim (H9 H8);split
                     [assumption
                     |intros;apply H12;apply in_list_cons;apply (in_list_filter ? ? ? H13)]]
-           |elim (decidable_eq_nat p t1)
-              [rewrite > H10;apply (ex_intro ? ? []);apply (ex_intro ? ? l1);
-               reflexivity
+           |elim (decidable_eq_nat p a)
+              [rewrite > H10;apply in_list_head
               |apply in_list_cons;elim (H2 p);apply (H12 H7 H8);intros;
-               apply (trans_le ? t1)
-                 [elim (decidable_lt p t1)
+               apply (trans_le ? a)
+                 [elim (decidable_lt p a)
                     [assumption
                     |lapply (not_lt_to_le ? ? H14);
-                     lapply (decidable_divides t1 p)
+                     lapply (decidable_divides a p)
                        [elim Hletin1
                           [elim H7;lapply (H17 ? H15)
                              [elim H10;symmetry;assumption
-                             |elim (H3 t1);elim H18
+                             |elim (H3 a);elim H18
                                 [elim H20;assumption
                                 |apply in_list_head]]
                           |elim (Not_lt_n_n p);apply H9;apply in_list_filter_r
-                             [elim (H3 p);apply (in_list_tail ? ? t1)
+                             [elim (H3 p);apply (in_list_tail ? ? a)
                                 [apply H17
                                    [apply prime_to_lt_SO;assumption
                                    |assumption
                                    |intros;elim H7;intro;lapply (H20 ? H21)
                                       [rewrite > Hletin2 in H18;elim (H11 H18);
-                                       lapply (H23 t1)
+                                       lapply (H23 a)
                                          [elim (lt_to_not_le ? ? Hletin3 Hletin)
-                                         |apply (ex_intro ? ? []);apply (ex_intro ? ? l);
-                                          reflexivity]
+                                         |apply in_list_head]
                                       |apply prime_to_lt_SO;elim (H2 p1);elim (H22 H18);
                                        elim H24;assumption]]
                                 |unfold;intro;apply H15;rewrite > H18;apply divides_n_n]
                              |rewrite > (not_divides_to_divides_b_false ? ? ? H15);
                                 [reflexivity
-                                |elim (H3 t1);elim H16
+                                |elim (H3 a);elim H16
                                    [elim H18;apply lt_to_le;assumption
                                    |apply in_list_head]]]]
-                       |elim (H3 t1);elim H15
+                       |elim (H3 a);elim H15
                           [elim H17;apply lt_to_le;assumption
                           |apply in_list_head]]]
                  |elim (in_list_cons_case ? ? ? ? H13)
                     [rewrite > H14;apply le_n
-                    |apply lt_to_le;apply (sorted_to_minimum ? ? ? H6);assumption]]]]
+                    |apply lt_to_le;apply (sorted_to_minimum ? ? ? ? H6);assumption]]]]
          |elim (H3 x);split;intros;
             [split 
                [elim H7
@@ -307,7 +189,7 @@ intro.elim t 0
                   [rewrite > H11;intro;lapply (in_list_filter_to_p_true ? ? ? H9);
                    rewrite > (divides_to_divides_b_true ? ? ? H12) in Hletin
                      [simplify in Hletin;destruct Hletin
-                     |elim (H3 t1);elim H13
+                     |elim (H3 a);elim H13
                         [elim H15;apply lt_to_le;assumption
                         |apply in_list_head]]
                   |elim H7
@@ -322,10 +204,10 @@ intro.elim t 0
                |intros;apply H11;apply in_list_cons;assumption
                |apply in_list_filter_r;
                   [assumption
-                  |lapply (H11 t1)
+                  |lapply (H11 a)
                      [rewrite > (not_divides_to_divides_b_false ? ? ? Hletin);
                         [reflexivity
-                        |elim (H3 t1);elim H13
+                        |elim (H3 a);elim H13
                            [elim H15;apply lt_to_le;assumption
                            |apply in_list_head]]
                      |apply in_list_head]]]]
@@ -335,41 +217,28 @@ intro.elim t 0
             [assumption
             |intros;unfold;elim (H2 y);elim (H8 H7);
              apply H11;apply in_list_head]
-         |generalize in match (sorted_cons_to_sorted ? ? ? H6);elim l
+         |generalize in match (sorted_cons_to_sorted ? ? ? ? H6);elim l
             [simplify;assumption
-            |simplify;elim (notb (divides_b t1 t2));simplify
-               [lapply (sorted_cons_to_sorted ? ? ? H8);lapply (H7 Hletin);
-                apply (sort_cons ? ? ? Hletin1);intros;
-                apply (sorted_to_minimum ? ? ? H8);apply (in_list_filter ? ? ? H9);
-               |apply H7;apply (sorted_cons_to_sorted ? ? ? H8)]]]]]
-qed.
-
-lemma in_list_singleton_to_eq : \forall A,x,y.in_list A x [y] \to x = y.
-intros;elim H;elim H1;generalize in match H2;elim a
-  [simplify in H3;destruct H3;reflexivity
-  |simplify in H4;destruct H4;generalize in match Hcut1;elim l
-     [simplify in H4;destruct H4
-     |simplify in H5;destruct H5]]
+            |simplify;elim (notb (divides_b a a1));simplify
+               [lapply (sorted_cons_to_sorted ? ? ? ? H8);lapply (H7 Hletin);
+                apply (sort_cons ? ? ? ? Hletin1);intros;
+                apply (sorted_to_minimum ? ? ? ? H8);apply (in_list_filter ? ? ? H9);
+               |apply H7;apply (sorted_cons_to_sorted ? ? ? ? H8)]]]]]
 qed.
 
 lemma le_list_n_aux_k_k : \forall n,m,k.in_list ? n (list_n_aux m k) \to
                           k \leq n.
 intros 2;elim m
   [simplify in H;elim (not_in_list_nil ? ? H)
-  |simplify in H1;elim H1;elim H2;generalize in match H3;elim a
-     [simplify in H4;destruct H4;apply le_n
-     |simplify in H5;destruct H5;apply lt_to_le;apply (H (S k));
-      apply (ex_intro ? ? l);apply (ex_intro ? ? a1);assumption]]
+  |simplify in H1;elim (in_list_cons_case ? ? ? ? H1)
+     [rewrite > H2;apply le_n
+     |apply lt_to_le;apply H;assumption]]
 qed.
 
 lemma in_list_SSO_list_n : \forall n.2 \leq n \to in_list ? 2 (list_n n).
-intros;elim H
-  [simplify;apply (ex_intro ? ? []);apply (ex_intro ? ? []);
-   simplify;reflexivity
-  |generalize in match H2;elim H1
-     [simplify;apply (ex_intro ? ? []);apply (ex_intro ? ? [3]);simplify;reflexivity
-     |simplify;apply (ex_intro ? ? []);apply (ex_intro ? ? (list_n_aux n2 3));
-      simplify;reflexivity]]
+intros;elim H;simplify
+  [apply in_list_head
+  |generalize in match H2;elim H1;simplify;apply in_list_head]
 qed.
 
 lemma le_SSO_list_n : \forall m,n.in_list nat n (list_n m) \to 2 \leq n.
@@ -379,11 +248,10 @@ qed.
 lemma le_list_n_aux : \forall n,m,k.in_list ? n (list_n_aux m k) \to n \leq k+m-1.
 intros 2;elim m
   [simplify in H;elim (not_in_list_nil ? ? H)
-  |simplify in H1;elim H1;elim H2;generalize in match H3;elim a
-     [simplify in H4;destruct H4;rewrite < plus_n_Sm;simplify;rewrite < minus_n_O;
+  |simplify in H1;elim (in_list_cons_case ? ? ? ? H1)
+     [rewrite > H2;rewrite < plus_n_Sm;simplify;rewrite < minus_n_O;
       rewrite > plus_n_O in \vdash (? % ?);apply le_plus_r;apply le_O_n
-     |simplify in H5;destruct H5;rewrite < plus_n_Sm;apply (H (S k));
-      apply (ex_intro ? ? l);apply (ex_intro ? ? a1);assumption]]
+     |rewrite < plus_n_Sm;apply (H (S k));assumption]]
 qed.
 
 lemma le_list_n : \forall n,m.in_list ? n (list_n m) \to n \leq m.
@@ -435,10 +303,11 @@ intro.elim n 0
      |intros;lapply (le_list_n_aux_k_k ? ? ? H1);assumption]]
 qed.
 
+definition list_of_primes \def \lambda n.\lambda l.
+\forall p.in_list nat p l  \to prime p \land p \leq n.
+
 lemma sieve_sound1 : \forall n.2 \leq n \to
-                               sorted_gt (sieve n) \land
-                               (\forall p.in_list ? p (sieve n) \to
-                               prime p \land p \leq n).
+sorted_gt (sieve n) \land list_of_primes n (sieve n).
 intros;elim (sieve_prime n n (list_n n) [])
   [split
      [assumption
@@ -471,9 +340,9 @@ lemma sieve_sorted : \forall n.sorted_gt (sieve n).
 intros;elim (decidable_le 2 n)
   [elim (sieve_sound1 ? H);assumption
   |generalize in match (le_S_S_to_le ? ? (not_le_to_lt ? ? H));cases n
-     [intro;apply sort_nil
+     [intro;simplify;apply sort_nil
      |intros;lapply (le_S_S_to_le ? ? H1);rewrite < (le_n_O_to_eq ? Hletin);
-      apply sort_nil]]
+      simplify;apply sort_nil]]
 qed.
 
 lemma in_list_sieve_to_prime : \forall n,p.2 \leq n \to in_list ? p (sieve n) \to
@@ -527,7 +396,7 @@ let rec checker l \def
 lemma checker_cons : \forall t,l.checker (t::l) = true \to checker l = true.
 intros 2;simplify;intro;generalize in match H;elim l
   [reflexivity
-  |change in H2 with (andb (checker (t1::l1)) (leb t (t1+(t1+O))) = true);
+  |change in H2 with (andb (checker (a::l1)) (leb t (a+(a+O))) = true);
    apply (andb_true_true ? ? H2)]
 qed.
 
@@ -546,6 +415,23 @@ definition bertrand \def \lambda n.
 definition not_bertrand \def \lambda n.
 \forall p.n < p \to p \le 2*n \to \not (prime p).
 
+(*
+lemma list_of_primes_SO: \forall l.list_of_primes 1 l \to
+l = [].
+intro.cases l;intros
+  [reflexivity
+  |apply False_ind.unfold in H.
+   absurd ((prime n) \land n \le 1)
+    [apply H.
+     apply in_list_head
+    |intro.elim H1.
+     elim H2.
+     apply (lt_to_not_le ? ? H4 H3)
+    ]
+  ]
+qed.
+*)
+
 lemma min_prim : \forall n.\exists p. n < p \land prime p \land
                  \forall q.prime q \to q < p \to q \leq n.
 intro;elim (le_to_or_lt_eq ? ? (le_O_n n))
@@ -571,6 +457,143 @@ intro;elim (le_to_or_lt_eq ? ? (le_O_n n))
       |intros;elim (lt_to_not_le ? ? H2);apply prime_to_lt_SO;assumption]]
 qed.
 
+theorem list_of_primes_to_bertrand: \forall n,pn,l.0 < n \to prime pn \to n <pn \to
+list_of_primes pn l  \to
+(\forall p. prime p \to p \le pn \to in_list nat p l) \to 
+(\forall p. in_list nat p l \to 2 < p \to
+\exists pp. in_list nat pp l \land pp < p \land p \le 2*pp) \to bertrand n.
+intros.
+elim (min_prim n).
+apply (ex_intro ? ? a).
+elim H6.clear H6.elim H7.clear H7.
+split
+  [split
+    [assumption
+    |elim (le_to_or_lt_eq ? ? (prime_to_lt_SO ? H9))
+      [elim (H5 a)
+        [elim H10.clear H10.elim H11.clear H11.
+         apply (trans_le ? ? ? H12).
+         apply le_times_r.
+         apply H8
+          [unfold in H3.
+           elim (H3 a1 H10).
+           assumption
+          |assumption
+          ]
+        |apply H4
+          [assumption
+          |apply not_lt_to_le.intro. 
+           apply (lt_to_not_le ? ? H2).
+           apply H8;assumption
+          ]
+        |assumption
+        ]
+      |rewrite < H7.
+       apply O_lt_const_to_le_times_const.
+       assumption
+      ]
+    ]
+  |assumption
+  ]
+qed.
+
+let rec check_list l \def
+  match l with
+  [ nil \Rightarrow true
+  | cons (hd:nat) tl \Rightarrow
+    match tl with
+     [ nil \Rightarrow eqb hd 2
+     | cons hd1 tl1 \Rightarrow 
+      (leb (S hd1) hd \land leb hd (2*hd1) \land check_list tl)
+    ]
+  ]
+.
+
+lemma check_list1: \forall n,m,l.(check_list (n::m::l)) = true \to 
+m < n \land n \le 2*m \land (check_list (m::l)) = true \land ((check_list l) = true).
+intros 3.
+change in ⊢ (? ? % ?→?) with (leb (S m) n \land leb n (2*m) \land check_list (m::l)).
+intro.
+lapply (andb_true_true ? ? H) as H1.
+lapply (andb_true_true_r ? ? H) as H2.clear H.
+lapply (andb_true_true ? ? H1) as H3.
+lapply (andb_true_true_r ? ? H1) as H4.clear H1.
+split
+  [split
+    [split
+      [apply leb_true_to_le.assumption
+      |apply leb_true_to_le.assumption
+      ]
+    |assumption
+    ]
+  |generalize in match H2.
+   cases l
+    [intro.reflexivity
+    |change in ⊢ (? ? % ?→?) with (leb (S n1) m \land leb m (2*n1) \land check_list (n1::l1)).
+     intro.
+     lapply (andb_true_true_r ? ? H) as H2.
+     assumption
+    ]
+  ]
+qed.
+    
+theorem check_list2: \forall l. check_list l = true \to
+\forall p. in_list nat p l \to 2 < p \to
+\exists pp. in_list nat pp l \land pp < p \land p \le 2*pp.
+intro.elim l 2
+  [intros.apply False_ind.apply (not_in_list_nil ? ? H1)
+  |cases l1;intros
+    [lapply (in_list_singleton_to_eq ? ? ? H2) as H4.
+     apply False_ind.
+     apply (lt_to_not_eq ? ? H3).
+     apply sym_eq.apply eqb_true_to_eq.
+     rewrite > H4.apply H1
+    |elim (check_list1 ? ? ? H1).clear H1.
+     elim H4.clear H4.
+     elim H1.clear H1.
+     elim (in_list_cons_case ? ? ? ? H2)
+      [apply (ex_intro ? ? n).
+       split
+        [split
+          [apply in_list_cons.apply in_list_head
+          |rewrite > H1.assumption
+          ]
+        |rewrite > H1.assumption
+        ]
+      |elim (H H6 p H1 H3).clear H.
+       apply (ex_intro ? ? a1). 
+       elim H8.clear H8.
+       elim H.clear H.
+       split
+        [split
+          [apply in_list_cons.assumption
+          |assumption
+          ]
+        |assumption
+        ]
+      ]
+    ]
+  ]
+qed.
+
+(* qualcosa che non va con gli S *)
+lemma le_to_bertrand : \forall n.O < n \to n \leq exp 2 8 \to bertrand n.
+intros.
+apply (list_of_primes_to_bertrand ? (S(exp 2 8)) (sieve (S(exp 2 8))))
+  [assumption
+  |apply primeb_true_to_prime.reflexivity
+  |apply (le_to_lt_to_lt ? ? ? H1).
+   apply le_n
+  |lapply (sieve_sound1 (S(exp 2 8))) as H
+    [elim H.assumption
+    |apply leb_true_to_le.reflexivity
+    ]
+  |intros.apply (sieve_sound2 ? ? H3 H2)
+  |apply check_list2.
+   reflexivity
+  ]
+qed.
+
 (*lemma pippo : \forall k,n.in_list ? (nth_prime (S k)) (sieve n) \to
               \exists l.sieve n = l@((nth_prime (S k))::(sieve (nth_prime k))).
 intros;elim H;elim H1;clear H H1;apply (ex_intro ? ? a);
@@ -578,6 +601,7 @@ cut (a1 = sieve (nth_prime k))
   [rewrite < Hcut;assumption
   |lapply (sieve_sorted n);generalize in match H2*) 
 
+(* old proof by Wilmer 
 lemma le_to_bertrand : \forall n.O < n \to n \leq exp 2 8 \to bertrand n.
 intros;
 elim (min_prim n);apply (ex_intro ? ? a);elim H2;elim H3;clear H2 H3;
@@ -660,7 +684,7 @@ split
             |apply prime_nth_prime
             |rewrite < H3;apply increasing_nth_prime]]]
    |assumption]
-qed.
+qed. *)
 
 lemma not_not_bertrand_to_bertrand1: \forall n.
 \lnot (not_bertrand n) \to \forall x. n \le x \to x \le 2*n \to