X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Fnat%2Fchebyshev.ma;h=701ad7ad16ac82b14a05a6c27ed14524d9b98552;hb=dc74ed7c4af1aa9b90fc5d2f0a86bd7825696e71;hp=317a82d15f2ebd3ae4b6648970cb3825ec3c7717;hpb=7265c6e8e0d548f6f97885727653b24c209d83f5;p=helm.git

diff --git a/helm/software/matita/library/nat/chebyshev.ma b/helm/software/matita/library/nat/chebyshev.ma
index 317a82d15..701ad7ad1 100644
--- a/helm/software/matita/library/nat/chebyshev.ma
+++ b/helm/software/matita/library/nat/chebyshev.ma
@@ -16,9 +16,207 @@ include "nat/log.ma".
 include "nat/pi_p.ma".
 include "nat/factorization.ma".
 include "nat/factorial2.ma".
+include "nat/o.ma".
 
 definition prim: nat \to nat \def
-\lambda n. sigma_p (S n) primeb (\lambda p.(S O)).
+\lambda n. sigma_p (S n) primeb (\lambda p.1).
+
+theorem le_prim_n: \forall n. prim n \le n.
+intros.unfold prim. elim n
+  [apply le_n
+  |apply (bool_elim ? (primeb (S n1)));intro
+    [rewrite > true_to_sigma_p_Sn
+      [rewrite > sym_plus.
+       rewrite < plus_n_Sm.
+       rewrite < plus_n_O.
+       apply le_S_S.assumption
+      |assumption
+      ]
+    |rewrite > false_to_sigma_p_Sn
+      [apply le_S.assumption
+      |assumption
+      ]
+    ]
+  ]
+qed.
+
+theorem not_prime_times_SSO: \forall n. 1 < n \to \lnot prime (2*n).
+intros.intro.elim H1.
+absurd (2 = 2*n)
+  [apply H3
+    [apply (witness ? ? n).reflexivity
+    |apply le_n
+    ]
+  |apply lt_to_not_eq.
+   rewrite > times_n_SO in ⊢ (? % ?).
+   apply lt_times_r.
+   assumption
+  ]
+qed.
+
+theorem eq_prim_prim_pred: \forall n. 1 < n \to 
+(prim (2*n)) = (prim (pred (2*n))).
+intros.unfold prim.
+rewrite < S_pred
+  [rewrite > false_to_sigma_p_Sn
+    [reflexivity
+    |apply not_prime_to_primeb_false.
+     apply not_prime_times_SSO.
+     assumption
+    ]
+  |apply (trans_lt ? (2*1))
+    [simplify.apply lt_O_S
+    |apply lt_times_r.
+     assumption
+    ]
+  ]
+qed.
+
+theorem le_prim_n1: \forall n. 4 \le n \to prim (S(2*n)) \le n.
+intros.unfold prim. elim H
+  [simplify.apply le_n
+  |cut (sigma_p (2*S n1) primeb (λp:nat.1) = sigma_p (S (2*S n1)) primeb (λp:nat.1))
+    [apply (bool_elim ? (primeb (S(2*(S n1)))));intro
+      [rewrite > true_to_sigma_p_Sn
+        [rewrite > sym_plus.
+         rewrite < plus_n_Sm.
+         rewrite < plus_n_O.
+         apply le_S_S.
+         rewrite < Hcut.
+         rewrite > times_SSO.
+         assumption
+        |assumption
+        ]
+      |rewrite > false_to_sigma_p_Sn
+        [apply le_S.
+         rewrite < Hcut.
+         rewrite > times_SSO.
+         assumption
+        |assumption
+        ]
+      ]
+    |apply sym_eq.apply (eq_prim_prim_pred (S n1)).
+     apply le_S_S.apply (trans_le ? 4)
+      [apply leb_true_to_le.reflexivity
+      |assumption
+      ]
+    ]
+  ]
+qed.
+
+(* usefull to kill a successor in bertrand *) 
+theorem le_prim_n2: \forall n. 7 \le n \to prim (S(2*n)) \le pred n.
+intros.unfold prim. elim H
+  [apply leb_true_to_le.reflexivity.
+  |cut (sigma_p (2*S n1) primeb (λp:nat.1) = sigma_p (S (2*S n1)) primeb (λp:nat.1))
+    [apply (bool_elim ? (primeb (S(2*(S n1)))));intro
+      [rewrite > true_to_sigma_p_Sn
+        [rewrite > sym_plus.
+         rewrite < plus_n_Sm.
+         rewrite < plus_n_O.
+         simplify in  ⊢ (? ? %).
+         rewrite > S_pred in ⊢ (? ? %)
+          [apply le_S_S.
+           rewrite < Hcut.
+           rewrite > times_SSO.
+           assumption
+          |apply (ltn_to_ltO ? ? H1)
+          ]
+        |assumption
+        ]
+      |rewrite > false_to_sigma_p_Sn
+        [simplify in  ⊢ (? ? %).
+         apply (trans_le ? ? ? ? (le_pred_n n1)).
+         rewrite < Hcut.
+         rewrite > times_SSO.
+         assumption
+        |assumption
+        ]
+      ]
+    |apply sym_eq.apply (eq_prim_prim_pred (S n1)).
+     apply le_S_S.apply (trans_le ? 4)
+      [apply leb_true_to_le.reflexivity
+      |apply (trans_le ? ? ? ? H1).
+       apply leb_true_to_le.reflexivity
+      ]
+    ]
+  ]
+qed.
+
+(* da spostare *)
+theorem le_pred: \forall n,m. n \le m \to pred n \le pred m.
+apply nat_elim2;intros
+  [apply le_O_n
+  |apply False_ind.apply (le_to_not_lt ? ? H).
+   apply lt_O_S
+  |simplify.apply le_S_S_to_le.assumption
+  ]
+qed.
+
+(* la prova potrebbe essere migliorata *)
+theorem le_prim_n3: \forall n. 15 \le n \to
+prim n \le pred (n/2).
+intros.
+elim (or_eq_eq_S (pred n)).
+elim H1
+  [cut (n = S (2*a))
+    [rewrite > Hcut.
+     apply (trans_le ? (pred a))
+      [apply le_prim_n2.
+       apply (le_times_to_le 2)
+        [apply le_n_Sn
+        |apply le_S_S_to_le.
+         rewrite < Hcut.
+         assumption
+        ]
+      |apply le_pred.
+       apply le_times_to_le_div
+        [apply lt_O_S
+        |apply le_n_Sn
+        ]
+      ]
+    |rewrite < H2.
+     apply S_pred.
+     apply (ltn_to_ltO ? ? H)
+    ]
+  |cut (n=2*(S a))
+    [rewrite > Hcut.
+     rewrite > eq_prim_prim_pred
+      [rewrite > times_SSO in ⊢ (? % ?).
+       change in ⊢ (? (? %) ?) with (S (2*a)).
+       rewrite > sym_times in ⊢ (? ? (? (? % ?))).
+       rewrite > lt_O_to_div_times
+        [apply (trans_le ? (pred a))
+          [apply le_prim_n2.
+           apply le_S_S_to_le.
+           apply (lt_times_to_lt 2)
+            [apply le_n_Sn
+            |apply le_S_S_to_le.
+             rewrite < Hcut.
+             apply le_S_S.
+             assumption
+            ]
+          |apply le_pred.
+           apply le_n_Sn
+          ]
+        |apply lt_O_S
+        ]
+      |apply le_S_S.
+       apply not_lt_to_le.intro.
+       apply (le_to_not_lt ? ? H).
+       rewrite > Hcut.
+       lapply (le_S_S_to_le ? ? H3) as H4.
+       apply (le_n_O_elim ? H4).
+       apply leb_true_to_le.reflexivity
+      ]
+    |rewrite > times_SSO.
+     rewrite > S_pred
+      [apply eq_f.assumption
+      |apply (ltn_to_ltO ? ? H)
+      ]
+    ]
+  ]
+qed.   
 
 (* This is chebishev psi function *)
 definition A: nat \to nat \def
@@ -134,7 +332,7 @@ elim n
     ]
   ]
 qed.
-    
+
 theorem lt_max_to_pi_p_primeb: \forall q,m. O < m \to max m (\lambda i.primeb i \land divides_b i m) < q \to
 m = pi_p q (\lambda i.primeb i \land divides_b i m) (\lambda p.exp p (ord m p)).
 intro.elim q
@@ -347,7 +545,7 @@ apply pi_p_primeb_divides_b.
 assumption.
 qed.
 
-theorem le_ord_log: \forall n,p. O < n \to S O < p \to
+theorem le_ord_log: \forall n,p. O < n \to 1 < p \to
 ord n p \le log p n.
 intros.
 rewrite > (exp_ord p) in ⊢ (? ? (? ? %))
@@ -458,7 +656,7 @@ qed.
 theorem eq_ord_sigma_p:
 \forall n,m,x. O < n \to prime x \to 
 exp x m \le n \to n < exp x (S m) \to
-ord n x=sigma_p m (λi:nat.divides_b (x\sup (S i)) n) (λx:nat.S O).
+ord n x=sigma_p m (λi:nat.divides_b (x\sup (S i)) n) (λx:nat.1).
 intros.
 lapply (prime_to_lt_SO ? H1).
 rewrite > (exp_ord x n) in ⊢ (? ? ? (? ? (λi:?.? ? %) ?))
@@ -600,20 +798,20 @@ pi_p (S n) primeb
 intros.
 rewrite > eq_fact_pi_p.
 apply (trans_eq ? ? 
-  (pi_p (S n) (λi:nat.leb (S O) i) 
-   (λn.pi_p (S n) primeb 
-    (\lambda p.(pi_p (log p n) 
-     (\lambda i.divides_b (exp p (S i)) n) (\lambda i.p))))))
+  (pi_p (S n) (λm:nat.leb (S O) m) 
+   (λm.pi_p (S m) primeb 
+    (\lambda p.(pi_p (log p m) 
+     (\lambda i.divides_b (exp p (S i)) m) (\lambda i.p))))))
   [apply eq_pi_p1;intros
     [reflexivity
     |apply pi_p_primeb1.
      apply leb_true_to_le.assumption
     ]
   |apply (trans_eq ? ? 
-    (pi_p (S n) (λi:nat.leb (S O) i)
-     (λn:nat
-      .pi_p (S n) (\lambda p.primeb p\land leb p n)
-       (λp:nat.pi_p (log p n) (λi:nat.divides_b ((p)\sup(S i)) n) (λi:nat.p)))))
+    (pi_p (S n) (λm:nat.leb (S O) m)
+     (λm:nat
+      .pi_p (S m) (\lambda p.primeb p\land leb p m)
+       (λp:nat.pi_p (log p m) (λi:nat.divides_b ((p)\sup(S i)) m) (λi:nat.p)))))
     [apply eq_pi_p1
       [intros.reflexivity
       |intros.apply eq_pi_p1
@@ -628,7 +826,7 @@ apply (trans_eq ? ?
         ]
       ]
     |apply (trans_eq ? ? 
-      (pi_p (S n) (λi:nat.leb (S O) i)
+      (pi_p (S n) (λm:nat.leb (S O) m)
        (λm:nat
         .pi_p (S n) (λp:nat.primeb p∧leb p m)
          (λp:nat.pi_p (log p m) (λi:nat.divides_b ((p)\sup(S i)) m) (λi:nat.p)))))
@@ -812,10 +1010,10 @@ intro.elim n
   |
 *)
 
-theorem fact_pi_p2: \forall n. fact ((S(S O))*n) =
-pi_p (S ((S(S O))*n)) primeb 
-  (\lambda p.(pi_p (log p ((S(S O))*n)) 
-    (\lambda i.true) (\lambda i.(exp p ((S(S O))*(n /(exp p (S i))))*(exp p (mod ((S(S O))*n /(exp p (S i))) (S(S O)))))))).
+theorem fact_pi_p2: \forall n. fact (2*n) =
+pi_p (S (2*n)) primeb 
+  (\lambda p.(pi_p (log p (2*n)) 
+    (\lambda i.true) (\lambda i.(exp p (2*(n /(exp p (S i))))*(exp p (mod (2*n /(exp p (S i))) 2)))))).
 intros.rewrite > fact_pi_p.
 apply eq_pi_p1
   [intros.reflexivity
@@ -834,13 +1032,13 @@ apply eq_pi_p1
   ]
 qed.
 
-theorem fact_pi_p3: \forall n. fact ((S(S O))*n) =
-pi_p (S ((S(S O))*n)) primeb 
-  (\lambda p.(pi_p (log p ((S(S O))*n)) 
-    (\lambda i.true) (\lambda i.(exp p ((S(S O))*(n /(exp p (S i))))))))*
-pi_p (S ((S(S O))*n)) primeb 
-  (\lambda p.(pi_p (log p ((S(S O))*n))   
-    (\lambda i.true) (\lambda i.(exp p (mod ((S(S O))*n /(exp p (S i))) (S(S O))))))).
+theorem fact_pi_p3: \forall n. fact (2*n) =
+pi_p (S (2*n)) primeb 
+  (\lambda p.(pi_p (log p (2*n)) 
+    (\lambda i.true) (\lambda i.(exp p (2*(n /(exp p (S i))))))))*
+pi_p (S (2*n)) primeb 
+  (\lambda p.(pi_p (log p (2*n))   
+    (\lambda i.true) (\lambda i.(exp p (mod (2*n /(exp p (S i))) 2))))).
 intros.
 rewrite < times_pi_p.
 rewrite > fact_pi_p2.
@@ -850,14 +1048,14 @@ apply eq_pi_p;intros
   ]
 qed.
 
-theorem pi_p_primeb4: \forall n. S O < n \to
-pi_p (S ((S(S O))*n)) primeb 
-  (\lambda p.(pi_p (log p ((S(S O))*n)) 
-    (\lambda i.true) (\lambda i.(exp p ((S(S O))*(n /(exp p (S i))))))))
+theorem pi_p_primeb4: \forall n. 1 < n \to
+pi_p (S (2*n)) primeb 
+  (\lambda p.(pi_p (log p (2*n)) 
+    (\lambda i.true) (\lambda i.(exp p (2*(n /(exp p (S i))))))))
 = 
 pi_p (S n) primeb 
-  (\lambda p.(pi_p (log p (S(S O)*n)) 
-    (\lambda i.true) (\lambda i.(exp p ((S(S O))*(n /(exp p (S i)))))))).
+  (\lambda p.(pi_p (log p (2*n)) 
+    (\lambda i.true) (\lambda i.(exp p (2*(n /(exp p (S i)))))))).
 intros.
 apply or_false_eq_SO_to_eq_pi_p
   [apply le_S_S.
@@ -879,14 +1077,14 @@ apply or_false_eq_SO_to_eq_pi_p
   ]
 qed.
    
-theorem pi_p_primeb5: \forall n. S O < n \to
-pi_p (S ((S(S O))*n)) primeb 
+theorem pi_p_primeb5: \forall n. 1 < n \to
+pi_p (S (2*n)) primeb 
   (\lambda p.(pi_p (log p ((S(S O))*n)) 
-    (\lambda i.true) (\lambda i.(exp p ((S(S O))*(n /(exp p (S i))))))))
+    (\lambda i.true) (\lambda i.(exp p (2*(n /(exp p (S i))))))))
 = 
 pi_p (S n) primeb 
   (\lambda p.(pi_p (log p n) 
-    (\lambda i.true) (\lambda i.(exp p ((S(S O))*(n /(exp p (S i)))))))).
+    (\lambda i.true) (\lambda i.(exp p (2*(n /(exp p (S i)))))))).
 intros.
 rewrite > (pi_p_primeb4 ? H).
 apply eq_pi_p1;intros
@@ -921,11 +1119,11 @@ apply eq_pi_p1;intros
 qed.
 
 theorem exp_fact_SSO: \forall n.
-exp (fact n) (S(S O))
+exp (fact n) 2
 = 
 pi_p (S n) primeb 
   (\lambda p.(pi_p (log p n) 
-    (\lambda i.true) (\lambda i.(exp p ((S(S O))*(n /(exp p (S i)))))))).
+    (\lambda i.true) (\lambda i.(exp p (2*(n /(exp p (S i)))))))).
 intros.
 rewrite > fact_pi_p.
 rewrite < exp_pi_p.
@@ -967,7 +1165,7 @@ reflexivity.
 qed.
 
 theorem eq_fact_B:\forall n.S O < n \to
-fact ((S(S O))*n) = exp (fact n) (S(S O)) * B((S(S O))*n).
+fact (2*n) = exp (fact n) 2 * B(2*n).
 intros. unfold B.
 rewrite > fact_pi_p3.
 apply eq_f2
@@ -1078,7 +1276,8 @@ cut ((S(S O)) < (S ((S(S(S(S O))))*n)))
     ]
   ]
 qed.
-             
+
+(* not usefull    
 theorem le_fact_A:\forall n.S O < n \to
 fact (2*n) \le exp (fact n) 2 * A (2*n).
 intros.
@@ -1087,7 +1286,7 @@ rewrite > eq_fact_B
    apply le_B_A
   |assumption
   ]
-qed.
+qed. *)
 
 theorem lt_SO_to_le_B_exp: \forall n.S O < n \to
 B (2*n) \le exp 2 (pred (2*n)).
@@ -1134,8 +1333,8 @@ apply (le_times_to_le (exp (fact n) (S(S O))))
   ]
 qed.
 
-theorem lt_SO_to_le_exp_B: \forall n. S O < n \to
-exp (S(S O)) ((S(S O))*n) \le (S(S O)) * n * B ((S(S O))*n).
+theorem lt_SO_to_le_exp_B: \forall n. 1 < n \to
+exp 2 (2*n) \le 2 * n * B (2*n).
 intros.
 apply (le_times_to_le (exp (fact n) (S(S O))))
   [apply lt_O_exp.
@@ -1153,7 +1352,7 @@ apply (le_times_to_le (exp (fact n) (S(S O))))
 qed.
 
 theorem le_exp_B: \forall n. O < n \to
-exp (S(S O)) ((S(S O))*n) \le (S(S O)) * n * B ((S(S O))*n).
+exp 2 (2*n) \le 2 * n * B (2*n).
 intros.
 elim H
   [apply le_n
@@ -1163,9 +1362,9 @@ elim H
 qed.
 
 theorem eq_A_SSO_n: \forall n.O < n \to
-A((S(S O))*n) =
- pi_p (S ((S(S O))*n)) primeb 
-  (\lambda p.(pi_p (log p ((S(S O))*n) )   
+A(2*n) =
+ pi_p (S (2*n)) primeb 
+  (\lambda p.(pi_p (log p (2*n) )   
     (\lambda i.true) (\lambda i.(exp p (bool_to_nat (leb (S n) (exp p (S i))))))))
  *A n.
 intro.
@@ -1261,7 +1460,7 @@ cut (
 qed.
                
 theorem le_A_BA1: \forall n. O < n \to 
-A((S(S O))*n) \le B((S(S O))*n)*A n.
+A(2*n) \le B(2*n)*A n.
 intros.
 rewrite > eq_A_SSO_n
   [apply le_times_l.
@@ -1511,23 +1710,6 @@ theorem A_SSSSO: A (S(S(S(S O)))) = S(S(S(S(S(S(S(S(S(S(S(S O))))))))))).
 reflexivity.
 qed.
 
-(* da spostare *)
-theorem or_eq_eq_S: \forall n.\exists m. 
-n = (S(S O))*m \lor n = S ((S(S O))*m).
-intro.elim n
-  [apply (ex_intro ? ? O).
-   left.reflexivity
-  |elim H.elim H1
-    [apply (ex_intro ? ? a).
-     right.apply eq_f.assumption
-    |apply (ex_intro ? ? (S a)).
-     left.rewrite > H2.
-     apply sym_eq.
-     apply times_SSO
-    ]
-  ]
-qed.
-
 (*
 (* a better result *)
 theorem le_A_exp3: \forall n. S O < n \to
@@ -1904,6 +2086,63 @@ elim (decidable_le 9 m)
   ]
 qed.       
 
+theorem le_exp_Al:\forall n. O < n \to exp 2 n \le A (2 * n).
+intros.
+apply (trans_le ? ((exp 2 (2*n))/(2*n)))
+  [apply le_times_to_le_div
+    [rewrite > (times_n_O O) in ⊢ (? % ?).
+     apply lt_times
+      [apply lt_O_S
+      |assumption
+      ]
+    |simplify in ⊢ (? ? (? ? %)).
+     rewrite < plus_n_O.
+     rewrite > exp_plus_times.
+     apply le_times_l.
+     apply le_times_SSO_n_exp_SSO_n
+    ]
+  |apply le_times_to_le_div2
+    [rewrite > (times_n_O O) in ⊢ (? % ?).
+     apply lt_times
+      [apply lt_O_S
+      |assumption
+      ]
+    |apply (trans_le ? ((B (2*n)*(2*n))))
+      [rewrite < sym_times in ⊢ (? ? %).
+       apply le_exp_B.
+       assumption
+      |apply le_times_l.
+       apply le_B_A
+      ]
+    ]
+  ]
+qed.
+
+theorem le_exp_A2:\forall n. 1 < n \to exp 2 (n / 2) \le A n.
+intros.
+apply (trans_le ? (A(n/2*2)))
+  [rewrite > sym_times.
+   apply le_exp_Al.
+   elim (le_to_or_lt_eq ? ? (le_O_n (n/2)))
+    [assumption
+    |apply False_ind.
+     apply (lt_to_not_le ? ? H).
+     rewrite > (div_mod n 2)
+      [rewrite < H1.
+       change in ⊢ (? % ?) with (n\mod 2).
+       apply le_S_S_to_le.
+       apply lt_mod_m_m.
+       apply lt_O_S
+      |apply lt_O_S
+      ]
+    ]
+  |apply monotonic_A.
+   rewrite > (div_mod n 2) in ⊢ (? ? %).
+   apply le_plus_n_r.
+   apply lt_O_S
+  ]
+qed.
+
 theorem eq_sigma_pi_SO_n: \forall n.
 sigma_p n (\lambda i.true) (\lambda i.S O) = n.
 intro.elim n
@@ -1946,13 +2185,13 @@ qed.
 
 (* the inequalities *)
 theorem le_exp_priml: \forall n. O < n \to
-exp (S(S O)) ((S(S O))*n) \le exp ((S(S O))*n) (S(prim ((S(S O))*n))).
+exp 2 (2*n) \le exp (2*n) (S(prim (2*n))).
 intros.
-apply (trans_le ? ((((S(S O))*n*(B ((S(S O))*n))))))
+apply (trans_le ? (((2*n*(B (2*n))))))
   [apply le_exp_B.assumption
-  |change in ⊢ (? ? %) with ((((S(S O))*n))*(((S(S O))*n))\sup (prim ((S(S O))*n))).
+  |change in ⊢ (? ? %) with (((2*n))*((2*n))\sup (prim (2*n))).
    apply le_times_r.
-   apply (trans_le ? (A ((S(S O))*n)))
+   apply (trans_le ? (A (2*n)))
     [apply le_B_A
     |apply le_Al
     ]
@@ -1987,7 +2226,7 @@ apply (trans_le ? (2*(4*n*(B (4*n)))))
 qed.
 
 theorem le_priml: \forall n. O < n \to
-(S(S O))*n \le (S (log (S(S O)) ((S(S O))*n)))*S(prim ((S(S O))*n)).
+2*n \le (S (log 2 (2*n)))*S(prim (2*n)).
 intros.
 rewrite < (eq_log_exp (S(S O))) in ⊢ (? % ?)
   [apply (trans_le ? ((log (S(S O)) (exp ((S(S O))*n) (S(prim ((S(S O))*n)))))))
@@ -2017,3 +2256,68 @@ apply (trans_le ? (exp (A n) 2))
   ]
 qed.
 
+(* bounds *)
+theorem le_primr: \forall n. 1 < n \to prim n \le 2*(2*n-3)/log 2 n.
+intros.
+apply le_times_to_le_div
+  [apply lt_O_log
+    [apply lt_to_le.assumption
+    |assumption
+    ]
+  |apply (trans_le ? (log 2 (exp n (prim n))))
+    [rewrite > sym_times.
+     apply log_exp2
+      [apply le_n
+      |apply lt_to_le.assumption
+      ]
+    |rewrite < (eq_log_exp 2) in ⊢ (? ? %)
+      [apply le_log
+        [apply le_n
+        |apply le_exp_primr
+        ]
+      |apply le_n
+      ]
+    ]
+  ]
+qed.
+     
+theorem le_priml1: \forall n. O < n \to
+2*n/((log 2 n)+2) - 1 \le prim (2*n).
+intros.
+apply le_plus_to_minus.
+apply le_times_to_le_div2
+  [rewrite > sym_plus.
+   simplify.apply lt_O_S
+  |rewrite > sym_times in ⊢ (? ? %).
+   rewrite < plus_n_Sm.
+   rewrite < plus_n_Sm in ⊢ (? ? (? ? %)).
+   rewrite < plus_n_O.
+   rewrite < sym_plus.
+   rewrite < log_exp
+    [simplify in ⊢ (? ? (? (? (? ? (? % ?))) ?)).
+     apply le_priml.
+     assumption
+    |apply le_n
+    |assumption
+    ]
+  ]
+qed.
+
+(*
+theorem prim_SSSSSSO: \forall n.30\le n \to O < prim (8*n) - prim n.
+intros.
+apply lt_to_lt_O_minus.
+change in ⊢ (? ? (? (? % ?))) with (2*4).
+rewrite > assoc_times.
+apply (le_to_lt_to_lt ? (2*(2*n-3)/log 2 n))
+  [apply le_primr.apply (trans_lt ? ? ? ? H).
+   apply leb_true_to_le.reflexivity
+  |apply (lt_to_le_to_lt ? (2*(4*n)/((log 2 (4*n))+2) - 1))
+    [elim H
+      [
+normalize in ⊢ (%);simplify.
+    |apply le_priml1.
+*)   
+
+
+