update in ground_2 and basic_2

[helm.git] / matita / matita / lib / arithmetics / chebyshev / bertrand.ma

diff --git a/matita/matita/lib/arithmetics/chebyshev/bertrand.ma b/matita/matita/lib/arithmetics/chebyshev/bertrand.ma
index d4a228a2c4dcaa21c9dca3b9617033519ff81cb8..8f41262e3b7519b5bb843605504e5a31c0ebc4e4 100644 (file)
--- a/matita/matita/lib/arithmetics/chebyshev/bertrand.ma
+++ b/matita/matita/lib/arithmetics/chebyshev/bertrand.ma
@@ -11,7 +11,7 @@
 
 include "arithmetics/sqrt.ma".
 include "arithmetics/chebyshev/psi_bounds.ma". 
-include "arithmetics/chebyshev/chebyshev_teta.ma". 
+include "arithmetics/chebyshev/chebyshev_theta.ma". 
 
 definition bertrand ≝ λn. ∃p.n < p ∧ p ≤ 2*n ∧ prime p.
 
@@ -166,7 +166,7 @@ elim (log p (2*n))
           [@leb_true_to_le //
           |>commutative_times in ⊢ (??%); > times_exp
            @(transitive_le ? (exp n 2))
-            [<associative_times >exp_2 in ⊢ (??%); @le_times //
+            [<associative_times >exp_2 in ⊢ (??%); @le_times [@le18|//]
             |@(le_exp1 … (lt_O_S ?))
              @(le_plus_to_le 3)
              cut (3+2*n/3*3 = S(2*n/3)*3) [//] #eq1 >eq1
@@ -189,9 +189,9 @@ elim (log p (2*n))
   ]
 qed.
         
-theorem le_B1_teta:∀n.18 ≤ n → not_bertrand n →
-  B1 (2*n) ≤ teta (2 * n / 3).
-#n #le18 #not_Bn >B1_def >teta_def
+theorem le_B1_theta:∀n.18 ≤ n → not_bertrand n →
+  B1 (2*n) ≤ theta (2 * n / 3).
+#n #le18 #not_Bn >B1_def >theta_def
 @(transitive_le ? (∏_{p < S (2*n) | primeb p} (p\sup(bool_to_nat (eqb (k (2*n) p) 1)))))
   [@le_pi #p #ltp #primebp @le_exp
     [@prime_to_lt_O @primeb_true_to_prime //
@@ -280,9 +280,9 @@ theorem not_bertrand_to_le_B:
   ∀n.exp 2 7 ≤ n → not_bertrand n →
   B (2*n) ≤ (exp 2 (2*(2 * n / 3)))*(exp (2*n) (pred(sqrt(2*n)/2))).
 #n #len #notB >eq_B_Bk >eq_Bk_B1_B2 @le_times
-  [@(transitive_le ? (teta ((2*n)/3)))
-    [@le_B1_teta [@(transitive_le … len) @leb_true_to_le //|//]
-    |@le_teta
+  [@(transitive_le ? (theta ((2*n)/3)))
+    [@le_B1_theta [@(transitive_le … len) @leb_true_to_le //|//]
+    |@le_theta
     ]
   |@le_B2_exp //
   ]
@@ -414,7 +414,7 @@ cut (0<n) [@(lt_to_le_to_lt … len) @lt_O_S] #posn
          <exp_S <plus_minus_m_m [2:@lt_O_log //]
          -Hind #Hind <Hclog @(transitive_le … Hind)
          >(eq_log_exp … (le_n ?)) >(eq_log_exp … (le_n ?))
-         >plus_minus_commutative [2:@lt_O_log //]
+         >plus_minus_associative [2:@lt_O_log //]
          cut (2+3 ≤ 2+log 2 m) 
           [@monotonic_le_plus_r @(le_exp_to_le 2) [@le_n|>Hclog @lt_to_le @lt8m]]
          generalize in match (2+log 2 m); #a #Hle >(commutative_times 2 a)