X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Fnat%2Fbertrand.ma;h=ce92ee4edc9d7015079831ff14314ae9c1f90aeb;hb=a79bf6edc13daaea8135ca71fdc92e02e229f030;hp=d3472d6758f31cfcaf90e8bbad5f6a9d89f751ee;hpb=5b83f526bc4c63424313df91173b844699eada96;p=helm.git

diff --git a/helm/software/matita/library/nat/bertrand.ma b/helm/software/matita/library/nat/bertrand.ma
index d3472d675..ce92ee4ed 100644
--- a/helm/software/matita/library/nat/bertrand.ma
+++ b/helm/software/matita/library/nat/bertrand.ma
@@ -15,8 +15,10 @@
 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".
+include "nat/sieve.ma".
 
 let rec list_divides l n \def
   match l with
@@ -32,282 +34,305 @@ 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
+let rec checker 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 ]].      
+      [ nil => true
+      | cons h1 t1 => match t1 with
+         [ nil => true
+         | cons h2 t2 => (andb (checker t1) (leb h1 (2*h2))) ]].
 
-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) ].
-      
-definition list_n : nat \to list nat \def
-  \lambda n.let rec aux n k \def
-    match n with
-    [ O => nil nat
-    | S n1 => k::aux n1 (S k) ]
-  in aux (pred n) 2.
-
-let rec sieve_aux l1 l2 t on t \def
-  match t with
-  [ O => l1
-  | S t1 => match l2 with
-    [ nil => l1
-    | cons n tl => sieve_aux (n::l1) (filter nat tl (\lambda x.notb (divides_b n x))) t1]].
-
-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]]
+lemma checker_cons : \forall t,l.checker (t::l) = true \to checker l = true.
+intros 2;simplify;intro;elim l in H ⊢ %
+  [reflexivity
+  |change in H1 with (andb (checker (a::l1)) (leb t (a+(a+O))) = true);
+   apply (andb_true_true ? ? H1)]
 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.
+theorem checker_sound : \forall l1,l2,l,x,y.l = l1@(x::y::l2) \to 
+                        checker l = true \to x \leq 2*y.
+intro;elim l1 0
+  [simplify;intros 5;rewrite > H;simplify;intro;
+   apply leb_true_to_le;apply (andb_true_true_r ? ? H1);
+  |simplify;intros;rewrite > H1 in H2;lapply (checker_cons ? ? H2);
+   apply (H l2 ? ? ? ? Hletin);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.
+definition bertrand \def \lambda n.
+\exists p.n < p \land p \le 2*n \land (prime p).
 
-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]]
+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.
-   
-axiom sieve_monotonic : \forall n.sieve (S n) = sieve n \lor sieve (S n) = (S n)::sieve n.
+*)
 
-axiom daemon : False.
+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))
+   [apply (ex_intro ? ? (min_aux (S (n!)) (S n) primeb));
+    split
+      [split
+         [apply le_min_aux;
+         |apply primeb_true_to_prime;apply f_min_aux_true;elim (ex_prime n);
+            [apply (ex_intro ? ? a);elim H1;elim H2;split
+               [split
+                  [assumption
+                  |rewrite > plus_n_O;apply le_plus
+                     [assumption
+                     |apply le_O_n]]
+               |apply prime_to_primeb_true;assumption]
+            |assumption]]
+      |intros;apply not_lt_to_le;intro;lapply (lt_min_aux_to_false ? ? ? ? H3 H2);
+       rewrite > (prime_to_primeb_true ? H1) in Hletin;destruct Hletin]
+   |apply (ex_intro ? ? 2);split
+      [split
+         [rewrite < H;apply lt_O_S
+         |apply primeb_true_to_prime;reflexivity]
+      |intros;elim (lt_to_not_le ? ? H2);apply prime_to_lt_SO;assumption]]
+qed.
 
-axiom in_list_cons_case : \forall A,x,a,l.in_list A x (a::l) \to
-                          x = a \lor in_list A x l.
-                          
-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
+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
-     [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]
+    [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.
 
-lemma in_list_head : \forall x,l.in_list nat x (x::l).
-intros;apply (ex_intro ? ? []);apply (ex_intro ? ? l);reflexivity;
-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 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]]
+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.
-
-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
-             (prime p \to p \leq k \to (\forall x.in_list ? x l2 \to p < x) \to in_list ? p l1)) \to
-  (\forall x.(in_list ? x l2 \to x \leq k \land \forall p.in_list ? p l1 \to \lnot p \divides x) \land
-             ((x \leq k \land \forall p.in_list ? p l1 \to \lnot p \divides x) \to
-              in_list ? x l2)) \to
-  length ? l2 \leq t \to
-  \forall p.(in_list ? p (sieve_aux l1 l2 t) \to prime p \land p \leq k) \land
-            (prime p \to p \leq k \to in_list ? p (sieve_aux l1 l2 t)).
-intro.elim t 0
-  [intros;cut (l2 = [])
-     [|generalize in match H2;elim l2
-        [reflexivity
-        |simplify in H4;elim (not_le_Sn_O ? H4)]]
-   simplify;split;intros;
-     [elim (H p);elim (H4 H3);assumption
-     |elim (H p);apply (H6 H3 H4);rewrite > Hcut;intros;unfold in H7;
-      elim H7;elim H8;clear H7 H8;generalize in match H9;elim a
-        [simplify in H7;destruct H7
-        |simplify in H8;destruct H8]]
-  |intros 4;elim l2
-     [simplify;split;intros
-        [elim (H1 p);elim (H5 H4);assumption
-        |elim (H1 p);apply (H7 H4 H5);intros;unfold in H8;
-         elim H8;elim H9;clear H8 H9;generalize in match H10;elim a
-           [simplify in H8;destruct H8
-           |simplify in H9;destruct H9]]
-     |simplify;elim (H k (filter ? l (\lambda x.notb (divides_b t1 x))) (t1::l1) ? ? ? p)
-        [split;intros
-           [apply H5;assumption
-           |apply H6;assumption]
-        |intro;split;intros
-           [elim (in_list_cons_case ? ? ? ? H5);
-              [rewrite > H6;split
-                 [split
-                    [unfold;intros;split
-                       [elim daemon (* aggiungere hp: ogni elemento di l2 è >= 2 *)
-                       |intros;elim (le_to_or_lt_eq ? ? (divides_to_le ? ? ? H7))
-                          [elim (divides_to_prime_divides ? ? H8 H9 H7);elim H10;
-                           elim H11;clear H10 H11;elim (H3 t1);elim H10
-                             [clear H10 H11;elim (H16 ? ? H12);elim (H2 a);clear H10;
-                              apply H11
-                                [assumption
-                                |apply (trans_le ? ? ? ? H15);
-                                 apply (trans_le ? ? ? H13);
-                                 apply lt_to_le;assumption
-                                |intros;
-                                 (* sfruttare il fatto che a < t1
-                                    e t1 è il minimo di t1::l *)
-                                 elim daemon]
-                             |unfold;apply (ex_intro ? ? []);
-                              apply (ex_intro ? ? l);
-                              reflexivity]
-                          |elim daemon (* aggiungere hp: ogni elemento di l2 è >= 2 *)
-                          |assumption]]
-                    |elim (H3 t1);elim H7
-                       [assumption
-                       |apply (ex_intro ? ? []);apply (ex_intro ? ? l);reflexivity]]
-                 |intros;elim (le_to_or_lt_eq t1 x)
-                    [assumption
-                    |rewrite > H8 in H7;lapply (in_list_filter_to_p_true ? ? ? H7);
-                     lapply (divides_n_n x);
-                     rewrite > (divides_to_divides_b_true ? ? ? Hletin1) in Hletin
-                       [simplify in Hletin;destruct Hletin
-                       |elim daemon (* aggiungere hp: ogni elemento di l2 è >= 2 *)]
-                    |(* sfruttare il fatto che t1 è il minimo di t1::l *)
-                     elim daemon]]
-                 |elim (H2 p1);elim (H7 H6);split
-                    [assumption
-                    |intros;apply H10;apply in_list_cons;apply (in_list_filter ? ? ? H11);]]
-           |elim (decidable_eq_nat p1 t1)
-              [rewrite > H8;apply (ex_intro ? ? []);apply (ex_intro ? ? l1);
-               reflexivity
-              |apply in_list_cons;elim (H2 p1);apply (H10 H5 H6);intros;
-               apply (trans_le ? t1)
-                 [elim (decidable_lt p1 t1)
-                    [assumption
-                    |lapply (not_lt_to_le ? ? H12);
-                     lapply (decidable_divides t1 p1)
-                       [elim Hletin1
-                          [elim H5;lapply (H15 ? H13)
-                             [elim H8;symmetry;assumption
-                             |(* per il solito discorso l2 >= 2 *)
-                              elim daemon]
-                          |elim (Not_lt_n_n p1);apply H7;apply in_list_filter_r
-                             [elim (H3 p1);apply (in_list_tail ? ? t1)
-                                [apply H15;split
-                                   [assumption
-                                   |intros;elim H5;intro;lapply (H18 ? H19)
-                                      [rewrite > Hletin2 in H16;elim (H9 H16);
-                                       lapply (H21 t1)
-                                         [elim (lt_to_not_le ? ? Hletin3 Hletin)
-                                         |apply (ex_intro ? ? []);apply (ex_intro ? ? l);
-                                          reflexivity]
-                                      |apply prime_to_lt_SO;elim (H2 p2);elim (H20 H16);
-                                       elim H22;assumption]]
-                                |unfold;intro;apply H13;rewrite > H16;apply divides_n_n;]
-                             |rewrite > (not_divides_to_divides_b_false ? ? ? H13);
-                                [reflexivity
-                                |elim daemon (* usare il solito >= 2 *)]]]
-                       |elim daemon (* come sopra *)]]
-                 |elim daemon (* t1::l è ordinata *)]]]
-         |intro;elim (H3 x);split;intros;
-            [split 
-               [elim H5
-                  [assumption
-                  |apply in_list_cons;apply (in_list_filter ? ? ? H7)]
-               |intros;elim (in_list_cons_case ? ? ? ? H8)
-                  [rewrite > H9;intro;lapply (in_list_filter_to_p_true ? ? ? H7);
-                   rewrite > (divides_to_divides_b_true ? ? ? H10) in Hletin
-                     [simplify in Hletin;destruct Hletin
-                     |elim daemon (* dal fatto che ogni elemento di t1::l è >= 2 *)]
-                  |elim H5
-                     [apply H11;assumption
-                     |apply in_list_cons;apply (in_list_filter ? ? ? H7)]]]
-            |elim H7;elim (in_list_cons_case ? ? ? ? (H6 ?))
-               [elim (H9 x)
-                  [rewrite > H10;unfold;
-                   apply (ex_intro ? ? []);apply (ex_intro ? ? l1);
-                   reflexivity
-                  |apply divides_n_n;]
-               |split
-                  [assumption
-                  |intros;apply H9;apply in_list_cons;assumption]
-               |apply in_list_filter_r;
-                  [assumption
-                  |lapply (H9 t1)
-                     [rewrite > (not_divides_to_divides_b_false ? ? ? Hletin);
-                        [reflexivity
-                        |(* solito >= 2 *)
-                         elim daemon]
-                     |apply in_list_head]]]]
-         |apply (trans_le ? ? ? (le_length_filter ? ? ?));apply le_S_S_to_le;
-          apply H4]]]
+    
+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.
 
-lemma sieve_soundness : \forall n.\forall p.
-                        in_list ? p (sieve n) \to
-                        p \leq n \land prime p.
-intros;unfold sieve in H;lapply (sieve_prime n (S n) (list_n n) [] ? ? ? p)
-  [intros;split;intros;
-     [elim daemon (* H1 is absurd *)
-     |elim daemon (* da sistemare, bisognerebbe raggiungere l'assurdo sapendo che p1 è primo e < 2 *)]
-  |intro;split;intros
-     [split
-        [elim daemon (* vero, dalla H1 *)
-        |intros;elim daemon (* H2 è assurda *)]
-     |elim H1;
-      (* vera supponendo x >= 2, il che in effetti è doveroso sistemare nel teoremone di prima *)
-      elim daemon]
-  |elim daemon (* sempre vero, da dimostrare *)
-  |elim Hletin;elim (H1 H);split
-     [elim daemon (* si può ottenere da H *)
-     |assumption]]
+(* 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.
 
-definition bertrand \def \lambda n.
-\exists p.n < p \land p \le 2*n \land (prime p).
+(*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);
+cut (a1 = sieve (nth_prime k))
+  [rewrite < Hcut;assumption
+  |lapply (sieve_sorted n);generalize in match H2*) 
 
-definition not_bertrand \def \lambda n.
-\forall p.n < p \to p \le 2*n \to \not (prime p).
+(* 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;
+cut (a \leq 257)
+  [|apply not_lt_to_le;intro;apply (le_to_not_lt ? ? H1);apply (H4 ? ? H2);
+    apply primeb_true_to_prime;reflexivity]
+split
+   [split
+      [assumption
+      |elim (prime_to_nth_prime a H6);generalize in match H2;cases a1
+         [simplify;intro;rewrite < H3;rewrite < plus_n_O;
+          change in \vdash (? % ?) with (1+1);apply le_plus;assumption
+         |intro;lapply (H4 (nth_prime n1))
+            [apply (trans_le ? (2*(nth_prime n1)))
+               [rewrite < H3;
+                cut (\exists l1,l2.sieve 257 = l1@((nth_prime (S n1))::((nth_prime n1)::l2)))
+                  [elim Hcut1;elim H7;clear Hcut1 H7;
+                   apply (checker_sound a2 a3 (sieve 257))
+                     [apply H8
+                     |reflexivity]
+                  |elim (sieve_sound2 257 (nth_prime (S n1)) ? ?)
+                     [elim (sieve_sound2 257 (nth_prime n1) ? ?)
+                        [elim H8;
+                         cut (\forall p.in_list ? p (a3@(nth_prime n1::a4)) \to prime p)
+                           [|rewrite < H9;intros;apply (in_list_sieve_to_prime 257 p ? H10);
+                            apply leb_true_to_le;reflexivity]
+                         apply (ex_intro ? ? a2);apply (ex_intro ? ? a4);
+                         elim H7;clear H7 H8;
+                         cut ((nth_prime n1)::a4 = a5)
+                           [|generalize in match H10;
+                             lapply (sieve_sorted 257);
+                             generalize in match Hletin1;
+                             rewrite > H9 in ⊢ (? %→? ? % ?→?);
+                             generalize in match Hcut1;
+                             generalize in match a2;
+                             elim a3 0
+                               [intro;elim l
+                                  [change in H11 with (nth_prime n1::a4 = nth_prime (S n1)::a5);
+                                   destruct H11;elim (eq_to_not_lt ? ? Hcut2);
+                                   apply increasing_nth_prime
+                                  |change in H12 with (nth_prime n1::a4 = t::(l1@(nth_prime (S n1)::a5)));
+                                   destruct H12;
+                                   change in H11 with (sorted_gt (nth_prime n1::l1@(nth_prime (S n1)::a5)));
+                                   lapply (sorted_to_minimum ? ? ? H11 (nth_prime (S n1)))
+                                     [unfold in Hletin2;elim (le_to_not_lt ? ? (lt_to_le ? ? Hletin2));
+                                      apply increasing_nth_prime
+                                     |apply (ex_intro ? ? l1);apply (ex_intro ? ? a5);reflexivity]]
+                               |intros 5;elim l1
+                                  [change in H12 with (t::(l@(nth_prime n1::a4)) = nth_prime (S n1)::a5);
+                                   destruct H12;cut (l = [])
+                                     [rewrite > Hcut2;reflexivity
+                                     |change in H11 with (sorted_gt (nth_prime (S n1)::(l@(nth_prime n1::a4))));
+                                      generalize in match H11;generalize in match H8;cases l;intros
+                                        [reflexivity
+                                        |lapply (sorted_cons_to_sorted ? ? ? H13);
+                                         lapply (sorted_to_minimum ? ? ? H13 n2)
+                                           [simplify in Hletin2;lapply (sorted_to_minimum ? ? ? Hletin2 (nth_prime n1))
+                                              [unfold in Hletin3;unfold in Hletin4;
+                                               elim (lt_nth_prime_to_not_prime ? ? Hletin4 Hletin3);
+                                               apply H12;
+                                               apply (ex_intro ? ? [nth_prime (S n1)]);
+                                               apply (ex_intro ? ? (l2@(nth_prime n1::a4)));
+                                               reflexivity
+                                              |apply (ex_intro ? ? l2);apply (ex_intro ? ? a4);reflexivity]
+                                           |simplify;apply in_list_head]]]
+                                  |change in H13 with (t::(l@(nth_prime n1::a4)) = t1::(l2@(nth_prime (S n1)::a5)));
+                                   destruct H13;apply (H7 l2 ? ? Hcut3)
+                                     [intros;apply H8;simplify;apply in_list_cons;
+                                      assumption
+                                     |simplify in H12;
+                                      apply (sorted_cons_to_sorted ? ? ? H12)]]]]
+                         rewrite > Hcut2 in ⊢ (? ? ? (? ? ? (? ? ? %)));
+                         apply H10
+                        |apply (trans_le ? ? ? Hletin);apply lt_to_le;
+                         apply (trans_le ? ? ? H5 Hcut)
+                        |apply prime_nth_prime]
+                     |rewrite > H3;assumption
+                     |apply prime_nth_prime]]
+               |apply le_times_r;assumption]
+            |apply prime_nth_prime
+            |rewrite < H3;apply increasing_nth_prime]]]
+   |assumption]
+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
@@ -585,7 +610,7 @@ qed.
         
 theorem le_B_split1_teta:\forall n.18 \le n \to not_bertrand n \to
 B_split1 (2*n) \le teta (2 * n / 3).
-intros.unfold B_split1.unfold teta.
+intros. unfold B_split1.unfold teta.
 apply (trans_le ? (pi_p (S (2*n)) primeb (λp:nat.(p)\sup(bool_to_nat (eqb (k (2*n) p) 1)))))
   [apply le_pi_p.intros.
    apply le_exp
@@ -1022,7 +1047,7 @@ rewrite > log_exp
   ]
 qed.
       
-theorem le_to_bertrand:
+theorem le_to_bertrand2:
 \forall n. (exp 2 8) \le n \to bertrand n.
 intros.
 apply not_not_bertrand_to_bertrand.unfold.intro.
@@ -1047,6 +1072,13 @@ absurd (2*n / 3 \le (sqrt(2*n)/2)*S(log 2 (2*n)))
   ]
 qed.
 
+theorem bertrand_n :
+\forall n. O < n \to bertrand n.
+intros;elim (decidable_le n 256)
+  [apply le_to_bertrand;assumption
+  |apply le_to_bertrand2;apply lt_to_le;apply not_le_to_lt;apply H1]
+qed.
+
 (* test 
 theorem mod_exp: eqb (mod (exp 2 8) 13) O = false.
 reflexivity.