From 342278d86d2ebb11b046dcc9f44cc5d08cd16352 Mon Sep 17 00:00:00 2001
From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Thu, 3 Jan 2013 16:15:54 +0000
Subject: [PATCH] Chebishev ported

---
 matita/matita/lib/arithmetics/bigops.ma       |  2 +-
 matita/matita/lib/arithmetics/binomial.ma     | 10 --
 .../lib/arithmetics/chebyshev/bertrand.ma     | 50 +++++-----
 .../lib/arithmetics/chebyshev/bertrand256.ma  | 96 +++++++------------
 .../lib/arithmetics/chebyshev/chebyshev.ma    | 23 ++---
 matita/matita/lib/arithmetics/log.ma          |  2 +-
 matita/matita/lib/arithmetics/minimization.ma | 19 +++-
 matita/matita/lib/arithmetics/ord.ma          | 11 +--
 matita/matita/lib/arithmetics/sqrt.ma         | 66 ++++++++++++-
 9 files changed, 155 insertions(+), 124 deletions(-)

diff --git a/matita/matita/lib/arithmetics/bigops.ma b/matita/matita/lib/arithmetics/bigops.ma
index a1b98e180..e51cd799a 100644
--- a/matita/matita/lib/arithmetics/bigops.ma
+++ b/matita/matita/lib/arithmetics/bigops.ma
@@ -163,7 +163,7 @@ op (\big[op,nil]_{i<k1|p1 i}(f i)) \big[op,nil]_{i<k2|p2 i}(g i) =
 qed.
 
 lemma plus_minus1: ∀a,b,c. c ≤ b → a + (b -c) = a + b -c.
-#a #b #c #lecb @sym_eq @plus_to_minus >(commutative_plus c)
+#a #b #c #lecb @sym_eq @plus_to_minus >(commutative_plus c) 
 >associative_plus <plus_minus_m_m //
 qed.
 
diff --git a/matita/matita/lib/arithmetics/binomial.ma b/matita/matita/lib/arithmetics/binomial.ma
index 74d2c8efd..c3834c8d8 100644
--- a/matita/matita/lib/arithmetics/binomial.ma
+++ b/matita/matita/lib/arithmetics/binomial.ma
@@ -191,13 +191,3 @@ cut (2 = 1+1) [//] #H2 >H2 in ⊢ (??(?%?));
   ]
 qed.
       
-(*
-theorem exp_Sn_SSO: \forall n. exp (S n) 2 = S((exp n 2) + 2*n).
-intros.simplify.
-rewrite < times_n_SO.
-rewrite < plus_n_O.
-rewrite < sym_times.simplify.
-rewrite < assoc_plus.
-rewrite < sym_plus.
-reflexivity.
-qed. *)
diff --git a/matita/matita/lib/arithmetics/chebyshev/bertrand.ma b/matita/matita/lib/arithmetics/chebyshev/bertrand.ma
index df94a30f6..d4a228a2c 100644
--- a/matita/matita/lib/arithmetics/chebyshev/bertrand.ma
+++ b/matita/matita/lib/arithmetics/chebyshev/bertrand.ma
@@ -10,8 +10,8 @@
       V_______________________________________________________________ *)
 
 include "arithmetics/sqrt.ma".
-include "arithmetics/chebyshev/chebyshev_B.ma".
-include "arithmetics/chebyshev/chebyshev_teta.ma".
+include "arithmetics/chebyshev/psi_bounds.ma". 
+include "arithmetics/chebyshev/chebyshev_teta.ma". 
 
 definition bertrand ≝ λn. ∃p.n < p ∧ p ≤ 2*n ∧ prime p.
 
@@ -85,38 +85,38 @@ theorem le_k: ∀n,p. k n p ≤ log p n.
   ]
 qed.
 
-definition B1 ≝ λn. 
+definition Bk ≝ λn. 
   ∏_{p < S n | primeb p}(exp p (k n p)).
   
-lemma B1_def : ∀n. B1 n = ∏_{p < S n | primeb p}(exp p (k n p)).
+lemma Bk_def : ∀n. Bk n = ∏_{p < S n | primeb p}(exp p (k n p)).
 // qed.
 
 definition Dexp ≝ mk_Dop nat 1 timesAC (λa,b.exp b a) ??.
   [// | normalize //]
 qed.
   
-theorem eq_B_B1: ∀n. B n = B1 n.
-#n >Bdef >B1_def @same_bigop
+theorem eq_B_Bk: ∀n. B n = Bk n.
+#n >Bdef >Bk_def @same_bigop
   [// |#i #ltiS #_ >k_def @exp_sigma_l]
 qed.
 
-definition B_split1 ≝ λn. 
+definition B1 ≝ λn. 
   ∏_{p < S n | primeb p}(exp p (bool_to_nat (leb (k n p) 1)* (k n p))).
 
-lemma B_split1_def : ∀n.
-  B_split1 n = ∏_{p < S n | primeb p}(exp p (bool_to_nat (leb (k n p) 1)* (k n p))).
+lemma B1_def : ∀n.
+  B1 n = ∏_{p < S n | primeb p}(exp p (bool_to_nat (leb (k n p) 1)* (k n p))).
 // qed.
 
-definition B_split2 ≝ λn. 
+definition B2 ≝ λn. 
   ∏_{p < S n | primeb p}(exp p (bool_to_nat (leb 2 (k n p))* (k n p))).
 
-lemma B_split2_def : ∀n.
-  B_split2 n = ∏_{p < S n | primeb p}(exp p (bool_to_nat (leb 2 (k n p))* (k n p))).
+lemma B2_def : ∀n.
+  B2 n = ∏_{p < S n | primeb p}(exp p (bool_to_nat (leb 2 (k n p))* (k n p))).
 // qed.
 
-theorem eq_B1_times_B_split1_B_split2: ∀n. 
-  B1 n = B_split1 n * B_split2 n.
-#n >B1_def >B_split1_def >B_split2_def <times_pi
+theorem eq_Bk_B1_B2: ∀n. 
+  Bk n = B1 n * B2 n.
+#n >Bk_def >B1_def >B2_def <times_pi
 @same_bigop
   [//
   |#p #ltp #primebp cases (true_or_false (leb (k n p) 1)) #Hc >Hc
@@ -189,9 +189,9 @@ elim (log p (2*n))
   ]
 qed.
         
-theorem le_B_split1_teta:∀n.18 ≤ n → not_bertrand n →
-  B_split1 (2*n) ≤ teta (2 * n / 3).
-#n #le18 #not_Bn >B_split1_def >teta_def
+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
 @(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 //
@@ -224,9 +224,9 @@ theorem le_B_split1_teta:∀n.18 ≤ n → not_bertrand n →
   ]
 qed.
 
-theorem le_B_split2_exp: ∀n. exp 2 7 ≤ n →
-  B_split2 (2*n) ≤ exp (2*n) (pred(sqrt(2*n)/2)).
-#n #len >B_split2_def
+theorem le_B2_exp: ∀n. exp 2 7 ≤ n →
+  B2 (2*n) ≤ exp (2*n) (pred(sqrt(2*n)/2)).
+#n #len >B2_def
 cut (O < n) [@(lt_to_le_to_lt … len) @leb_true_to_le //] #posn
 @(transitive_le ? 
    (∏_{p < S (sqrt (2*n)) | primeb p}
@@ -279,12 +279,12 @@ qed.
 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_B1 >eq_B1_times_B_split1_B_split2 @le_times
+#n #len #notB >eq_B_Bk >eq_Bk_B1_B2 @le_times
   [@(transitive_le ? (teta ((2*n)/3)))
-    [@le_B_split1_teta [@(transitive_le … len) @leb_true_to_le //|//]
+    [@le_B1_teta [@(transitive_le … len) @leb_true_to_le //|//]
     |@le_teta
     ]
-  |@le_B_split2_exp //
+  |@le_B2_exp //
   ]
 qed.
 
@@ -429,7 +429,7 @@ cut (0<n) [@(lt_to_le_to_lt … len) @lt_O_S] #posn
   ]
 qed.
 
-theorem le_to_bertrand2:
+theorem bertrand_up:
    ∀n. 2^8 ≤ n → bertrand n.
 #n #len @not_not_bertrand_to_bertrand % #notBn
 @(absurd (2*n / 3 \le (sqrt(2*n)/2)*S(log 2 (2*n))))
diff --git a/matita/matita/lib/arithmetics/chebyshev/bertrand256.ma b/matita/matita/lib/arithmetics/chebyshev/bertrand256.ma
index fd31e2a29..163125b81 100644
--- a/matita/matita/lib/arithmetics/chebyshev/bertrand256.ma
+++ b/matita/matita/lib/arithmetics/chebyshev/bertrand256.ma
@@ -155,81 +155,57 @@ lemma primes_below_lop: ∀n. primes_below (list_of_primes n) (n+2).
 #n @lprim_invariant //
 qed.
 
-let rec checker l ≝
-  match l with
-    [ nil ⇒  true
-    | cons h1 t1 => match t1 with
-      [ nil ⇒  true
-      | cons h2 t2 ⇒ (andb (checker t1) (leb h1 (2*h2))) ]].
-
-lemma checker_ab: ∀a,b,l. 
-  checker (a::b::l) = (andb (checker (b::l)) (leb a (2*b))).
-// qed.
-
-lemma checker_cons : ∀a,l.checker (a::l) = true → checker l = true.
-#a #l cases l [//|#b #tl >checker_ab #H @(andb_true_l ?? H)]
-qed.
-
-theorem list_of_primes_to_bertrand: 
-∀n,pn,l.0 < n → prime pn → n < pn → all_primes l  →
-(∀p. prime p → p ≤ pn → mem ? p l) → 
-(∀p. mem ? p l → 2 < p →
-  ∃pp. mem ? pp l ∧ pp < p ∧ p \le 2*pp) → bertrand n.
-#n #pn #l #posn #primepn #ltnp #allprimes #H1 #H2 
+(* check *)
+theorem primes_below_to_bertrand: 
+∀pm,l.prime pm → primes_below l (S pm)  →
+  (∀p. mem ? p l → 2 < p → ∃pp. mem ? pp l ∧ pp < p ∧ p ≤ 2*pp) 
+    → ∀n.0 < n → n < pm → bertrand n.
+#pm #l #primepm * * #Hall #Hbelow #Hcomplete #H #n #posn #ltn  
 cases (min_prim n) #p1 * * #ltnp1 #primep1 #Hmin
 %{p1} % // % [//] 
 cases(le_to_or_lt_eq ? ? (prime_to_lt_SO ? primep1)) #Hp1
-  [cases (H2 … Hp1)
-    [#x * * #memxl #ltxp1 #H @(transitive_le … H) @monotonic_le_times_r 
-     @Hmin [@allprimes //|//]
-    |@H1 [//] @not_lt_to_le % #ltpn @(absurd ? ltnp)
+  [cases (H … Hp1)
+    [#x * * #memxl #ltxp1 #Hp1 @(transitive_le … Hp1) @monotonic_le_times_r 
+     @Hmin [@Hall //|//]
+    |@Hcomplete [//] @le_S_S @not_lt_to_le % #ltpm @(absurd ? ltn)
      @le_to_not_lt @Hmin //
     ]
   |<Hp1 >(times_n_1 2) in ⊢ (?%?); @monotonic_le_times_r //
   ]
 qed.
 
-let rec check_list l ≝
+let rec checker l ≝
   match l with
   [ nil ⇒ true
-  | cons (hd:nat) tl ⇒
+  | cons hd tl ⇒
     match tl with
      [ nil ⇒ true
      | cons hd1 tl1 ⇒ 
-      (leb (S hd) hd1 ∧ leb hd1 (2*hd) ∧ check_list tl)
+       leb (S hd) hd1 ∧ leb hd1 (2*hd) ∧ checker tl
     ]
-  ]
-.
+  ].
 
-lemma check_list_ab: ∀a,b,l.check_list (a::b::l) =
-  (leb (S a) b ∧ leb b (2*a) ∧ check_list (b::l)).
+lemma checker_ab: ∀a,b,l.checker (a::b::l) =
+  (leb (S a) b ∧ leb b (2*a) ∧ checker (b::l)).
 // qed.
 
-lemma check_list_abl: ∀a,b,l.check_list (a::b::l) = true →
-  a < b ∧ 
-  b ≤ 2*a ∧ 
-  check_list (b::l) = true ∧ 
-  check_list l = true.
-#a #b #l >check_list_ab #H 
-lapply (andb_true_r ?? H) #H1
-lapply (andb_true_l ?? H) -H #H2 
-lapply (andb_true_r ?? H2) #H3 
-lapply (andb_true_l ?? H2) -H2 #H4
-% [% [% [@(leb_true_to_le … H4) |@(leb_true_to_le … H3)]|@H1]
-  |lapply H1 cases l
-    [//
-    |#c #d >check_list_ab #H @(andb_true_r … H)
-    ]
+lemma checker_abl: ∀a,b,l.checker (a::b::l) = true →
+  a < b ∧ b ≤ 2*a ∧ checker (b::l) = true.
+#a #b #l >checker_ab #H 
+% [% [@leb_true_to_le @(andb_true_l … (andb_true_l … H))
+     |@leb_true_to_le @(andb_true_r … (andb_true_l … H))
+     ]
+  |@(andb_true_r … H)
   ]
 qed.
     
-theorem check_list_spec: ∀tl,a,l. check_list l = true → l = a::tl →
+theorem checker_spec: ∀tl,a,l. checker l = true → l = a::tl →
   ∀p. mem ? p tl → ∃pp. mem nat pp l ∧ pp < p ∧ p ≤ 2*pp.
 #tl elim tl
   [#a #l #_ #_ #p whd in ⊢ (%→?); @False_ind 
   |#b #tl #Hind #a #l #Hc #Hl #p #Hmem >Hl in Hc;
-   #Hc cases(check_list_abl … Hc) * * 
-   #ltab #leb #Hc2 #Hc3 cases Hmem #Hc
+   #Hc cases(checker_abl … Hc) *  
+   #ltab #leb #Hc2 cases Hmem #Hc
     [>Hc -Hc %{a} % [ % [ % % |//]|//]
     |cases(Hind b (b::tl) Hc2 (refl …) ? Hc) #pp * * #Hmemnp #ltpp #lepp
      %{pp} % [ % [ %2 //|//]|//]
@@ -237,17 +213,14 @@ theorem check_list_spec: ∀tl,a,l. check_list l = true → l = a::tl →
   ]
 qed.
 
-lemma le_to_bertrand : ∀n.O < n → n ≤ 2^8 → bertrand n.
+lemma bertrand_down : ∀n.O < n → n ≤ 2^8 → bertrand n.
 #n #posn #len
 cut (∃it.it=2^8) [%{(2^8)} %] * #it #itdef
 lapply(primes_below_lop … it) * * #Hall #Hbelow #Hcomplete
-@(list_of_primes_to_bertrand ? (S it) (list_of_primes it) posn)
+@(primes_below_to_bertrand (S it) (list_of_primes it) … posn)
   [@primeb_true_to_prime >itdef %
-  |@le_S_S >itdef @len
-  |@Hall
-  |#p #primep #lep @Hcomplete 
-    [@primep |<plus_n_Sm @le_S_S <plus_n_Sm <plus_n_O @lep]
-  |#p #memp #lt2p @(check_list_spec (tail ? (list_of_primes it)) 2 (list_of_primes it))
+  |>(plus_n_O it) in ⊢ (??%); >plus_n_Sm >plus_n_Sm @primes_below_lop
+  |#p #memp #lt2p @(checker_spec (tail ? (list_of_primes it)) 2 (list_of_primes it))
     [>itdef %
     |>itdef @eq_lop @lt_O_S 
     |>eq_lop in memp; [2:>itdef @lt_O_S] * 
@@ -255,17 +228,14 @@ lapply(primes_below_lop … it) * * #Hall #Hbelow #Hcomplete
       |#H @H
       ]
     ]
+  |@le_S_S >itdef @len
   ]
 qed.
 
-theorem bertrand_n :
+theorem bertrand :
 ∀n. O < n → bertrand n.
 #n #posn elim (decidable_le n 256)
-  [@le_to_bertrand //
+  [@bertrand_down //
   |#len @le_to_bertrand2 @lt_to_le @not_le_to_lt @len]
 qed.
 
-(* test 
-theorem mod_exp: eqb (mod (exp 2 8) 13) O = false.
-reflexivity.
-*)
diff --git a/matita/matita/lib/arithmetics/chebyshev/chebyshev.ma b/matita/matita/lib/arithmetics/chebyshev/chebyshev.ma
index 4195de34b..50fb09fd7 100644
--- a/matita/matita/lib/arithmetics/chebyshev/chebyshev.ma
+++ b/matita/matita/lib/arithmetics/chebyshev/chebyshev.ma
@@ -90,24 +90,24 @@ theorem le_prim_n3: ∀n. 15 ≤ n →
 qed. 
 
 (* This is chebishev psi function *)
-definition A: nat → nat ≝
+definition Psi: nat → nat ≝
   λn.∏_{p < S n | primeb p} (exp p (log p n)).
   
 definition psi_def : ∀n. 
-  A n = ∏_{p < S n | primeb p} (exp p (log p n)).
+  Psi n = ∏_{p < S n | primeb p} (exp p (log p n)).
 // qed.
 
-theorem le_Al1: ∀n.
-  A n ≤ ∏_{p < S n | primeb p} n.
+theorem le_Psil1: ∀n.
+  Psi n ≤ ∏_{p < S n | primeb p} n.
 #n cases n [@le_n |#m @le_pi #i #_ #_ @le_exp_log //]
 qed.
 
-theorem le_Al: ∀n. A n ≤ exp n (prim n).
-#n <exp_sigma @le_Al1
+theorem le_Psil: ∀n. Psi n ≤ exp n (prim n).
+#n <exp_sigma @le_Psil1
 qed.
 
-theorem leA_r2: ∀n.
-  exp n (prim n) ≤ A n * A n.
+theorem lePsi_r2: ∀n.
+  exp n (prim n) ≤ Psi n * Psi n.
 #n elim (le_to_or_lt_eq ?? (le_O_n n)) #Hn
   [<(exp_sigma (S n) n primeb) <times_pi
    @le_pi #i #lti #primei 
@@ -129,13 +129,13 @@ theorem leA_r2: ∀n.
 qed.
 
 (* an equivalent formulation for psi *)
-definition A': nat → nat ≝
+definition Psi': nat → nat ≝
 λn. ∏_{p < S n | primeb p} (∏_{i < log p n} p).
 
-lemma Adef: ∀n. A' n = ∏_{p < S n | primeb p} (∏_{i < log p n} p).
+lemma Psidef: ∀n. Psi' n = ∏_{p < S n | primeb p} (∏_{i < log p n} p).
 // qed-.
 
-theorem eq_A_A': ∀n.A n = A' n.
+theorem eq_Psi_Psi': ∀n.Psi n = Psi' n.
 #n @same_bigop // #i #lti #primebi
 @(trans_eq ? ? (exp i (∑_{x < log i n} 1)))
   [@eq_f @sym_eq @sigma_const
@@ -315,6 +315,7 @@ theorem pi_p_primeb: ∀n. O < n →
 #n #posn <eq_pi_p_primeb_divides_b @pi_p_primeb_dividesb //
 qed.
 
+(* more result on order functions *)
 theorem le_ord_log: ∀n,p. O < n → 1 < p →
   ord n p ≤ log p n.
 #n #p #posn #lt1p >(exp_ord p ? lt1p posn) in ⊢ (??(??%)); 
diff --git a/matita/matita/lib/arithmetics/log.ma b/matita/matita/lib/arithmetics/log.ma
index 733720ce3..bbd65be96 100644
--- a/matita/matita/lib/arithmetics/log.ma
+++ b/matita/matita/lib/arithmetics/log.ma
@@ -140,7 +140,7 @@ theorem log_exp: ∀p,n,m. 1 < p → O < m →
   |#i #Hi #Hm @lt_to_leb_false
    @(lt_to_le_to_lt ? ((exp p n)*(exp p (S(log p m)))))
     [@monotonic_lt_times_r [@lt_O_exp @lt_to_le // |@lt_exp_log //]
-    |<exp_plus_times @le_exp [@lt_to_le // |<plus_n_Sm //]
+    |<exp_plus_times @le_exp [@lt_to_le // | //]
     ]
   ]
 qed.
diff --git a/matita/matita/lib/arithmetics/minimization.ma b/matita/matita/lib/arithmetics/minimization.ma
index 5d4fc9bce..526539b24 100644
--- a/matita/matita/lib/arithmetics/minimization.ma
+++ b/matita/matita/lib/arithmetics/minimization.ma
@@ -123,7 +123,7 @@ theorem max_f_g: ∀f,g,n.(∀i. i < n → f i = g i) →
   max n f = max n g.
 #f #g #n (elim n) //
 #m #Hind #ext normalize >ext normalize in Hind; >Hind //
-#i #ltim @ext /2/
+#i #ltim @ext @le_S //
 qed.
 
 theorem le_max_f_max_g: ∀f,g,n. (∀i. i < n → f i = true → g i =true) →
@@ -131,7 +131,7 @@ max n f ≤ max n g.
 #f #g #n (elim n) //
 #m #Hind #ext normalize (cases (true_or_false (f m))) #Heq >Heq 
   [>ext //
-  |(cases (g m)) normalize [@le_max_n] @Hind #i #ltim @ext /2/
+  |(cases (g m)) normalize [@le_max_n] @Hind #i #ltim @ext @le_S //
 qed.
 
 theorem f_max_true : ∀ f.∀n.
@@ -173,6 +173,17 @@ cases (exists_forall_lt f n)
   ]
 qed.
 
+
+theorem false_to_lt_max: ∀f,n,m.O < n →
+  f n = false → max m f ≤ n → max m f < n.
+#f #n #m #posn #Hfn #Hmax cases (le_to_or_lt_eq ?? Hmax) -Hmax #Hmax 
+  [//
+  |cases (exists_max_forall_false f m)
+    [* #_ #Hfmax @False_ind @(absurd ?? not_eq_true_false) //
+    |* //
+    ]
+  ]
+qed.
 (* minimization *)
  
 (* min k b f is the minimun i, b ≤ i < b + k s.t. f i;  
@@ -318,7 +329,7 @@ theorem min_f_g: ∀f,g,n,b.(∀i. b ≤ i → i < n + b → f i = g i) →
   min n b f = min n b g.
 #f #g #n (elim n) //
 #m #Hind #b #ext normalize >(ext b (le_n b) ?) // >Hind //
-#i #ltib #ltim @ext /2/
+#i #ltib #ltim @ext // @lt_to_le //
 qed.
 
 theorem le_min_f_min_g: ∀f,g,n,b. (∀i. b ≤ i → i < n +b → f i = true → g i =true) →
@@ -326,7 +337,7 @@ min n b g ≤ min n b f.
 #f #g #n (elim n) //
 #m #Hind #b #ext normalize (cases (true_or_false (f b))) #Heq >Heq 
   [>ext //
-  |(cases (g b)) normalize /2/ @Hind #i #ltb #ltim #fi
+  |(cases (g b)) normalize /2 by lt_to_le/ @Hind #i #ltb #ltim #fi
     @ext /2/
   ]
 qed.
diff --git a/matita/matita/lib/arithmetics/ord.ma b/matita/matita/lib/arithmetics/ord.ma
index 452106f78..bd1a17161 100644
--- a/matita/matita/lib/arithmetics/ord.ma
+++ b/matita/matita/lib/arithmetics/ord.ma
@@ -13,10 +13,6 @@ include "arithmetics/exp.ma".
 include "basics/types.ma".
 include "arithmetics/primes.ma".
 include "arithmetics/gcd.ma". 
-(*
-include "arithmetics/nth_prime.ma".
-(* for some properties of divides *)
-*)
 
 let rec p_ord_aux p n m ≝
   match n \mod m with
@@ -54,8 +50,7 @@ qed.
 lemma p_ord_degenerate: ∀p,n. p_ord_aux p n 1 = 〈p,n〉.
 #p elim p // #p1 #Hind #n
 cut (mod n 1 = 0) [@divides_to_mod_O //] #Hmod
->(p_ord_aux_Strue … (Hind … ) ) // >(div_mod n 1) in ⊢ (???%);
->Hmod <plus_n_O <times_n_1 //
+>(p_ord_aux_Strue … (Hind … ) ) // >(div_mod n 1) in ⊢ (???%); //
 qed.
 
 theorem p_ord_aux_to_exp: ∀p,n,m,q,r. O < m →
@@ -170,7 +165,7 @@ elim (p_ord_to_exp1 ???? Hp1 posb pordb) -posb -pordb #Hdivb #Hb
   [@lt_to_le //
   |% #Hdiv cases (divides_times_to_divides ? ? ? Hprime Hdiv)
    #Habs @absurd /2/
-  |>Ha >Hb -Ha -Hb <associative_times <associative_times // 
+  |>Ha >Hb -Ha -Hb // 
   ]
 qed.
 
@@ -221,7 +216,7 @@ cases (p_ord_to_exp1 ? ? ? ? Hposp posm ordm) #divm #eqm %
          >commutative_gcd @eq_gcd_times_1
           [@lt_O_exp @lt_to_le // 
           |@lt_to_le //
-          |>commutative_gcd //
+          |/2/ 
           |>commutative_gcd @prime_to_gcd_1 //
           ]
         ]
diff --git a/matita/matita/lib/arithmetics/sqrt.ma b/matita/matita/lib/arithmetics/sqrt.ma
index 7bb9282f0..eb243605c 100644
--- a/matita/matita/lib/arithmetics/sqrt.ma
+++ b/matita/matita/lib/arithmetics/sqrt.ma
@@ -84,7 +84,7 @@ lemma le_sqrt_n1: ∀n. n - 2*sqrt n ≤ exp (sqrt n) 2.
 #n  @le_plus_to_minus @le_S_S_to_le
 cut (S ((sqrt n)\sup 2+2*sqrt n) = (exp (S(sqrt n)) 2))
   [2:#Hcut >Hcut @lt_sqrt]
->exp_2 >exp_2 generalize in match (sqrt n); #a 
+>exp_2 >exp_2 generalize in match (sqrt n); #a  
 normalize // 
 qed.
 
@@ -146,6 +146,70 @@ lemma le_sqrt_log_n : ∀n,b. 2 < b → sqrt n * log b n ≤ n.
 @monotonic_le_times_r @le_sqrt_log //
 qed.
 
+theorem le_square_exp:∀n. 3 < n → exp n 2 ≤ exp 2 n.
+#n #lt3n elim lt3n
+  [@le_n
+  |#m #le4m #Hind normalize <plus_n_O >commutative_times
+   normalize <(commutative_times 2) normalize <associative_plus
+   <plus_n_O >commutative_plus >plus_n_Sm @le_plus 
+     [<exp_2 @Hind
+     |elim le4m [@leb_true_to_le //]
+      #m1 #lem1 #Hind1 normalize >commutative_times normalize 
+      <plus_n_O <plus_n_Sm >(plus_n_O (S(m1+m1))) >plus_n_Sm >plus_n_Sm
+      @le_plus [@Hind1 |>(exp_n_1 2) in ⊢ (?%?); @le_exp 
+       [@lt_O_S |@(transitive_le … lem1) @leb_true_to_le //]
+     ]
+   ]
+ ]
+qed.
+
+lemma le_log2_sqrt: ∀n. 2^4 ≤ n→ log 2 n ≤ sqrt n.
+#n #le_n >sqrt_def 
+@true_to_le_max
+  [@le_S_S @le_log_n_n //
+  |@le_to_leb_true 
+   cut (0<n) [@(transitive_lt … le_n) @lt_O_S] #posn
+   @(transitive_le … (le_exp_log 2 n posn))
+   <exp_2 @le_square_exp @true_to_le_max
+    [@(lt_to_le_to_lt … le_n) @leb_true_to_le // |@le_to_leb_true //]
+  ]
+qed.
+
+lemma square_S: ∀a. (S a)^2 = a^2 + 2*a +1.
+#a normalize >commutative_times normalize //
+qed. 
+
+theorem le_squareS_exp:∀n. 5 < n → exp (S n) 2 ≤ exp 2 n.
+#n #lt4n elim lt4n
+  [@leb_true_to_le //
+  |#m #le4m #Hind >square_S whd in ⊢(??%); >commutative_times in ⊢(??%);
+   normalize in ⊢(??%); <plus_n_O >associative_plus @le_plus [@Hind]
+   elim le4m [@leb_true_to_le //] #a #lea #Hinda
+   @(transitive_le ? (2*(2*(S a)+1)))
+    [@lt_to_le whd >plus_n_Sm >(times_n_1 2) in ⊢ (?(??%)?);
+     <distributive_times_plus @monotonic_le_times_r @le_plus [2://] 
+     normalize // 
+    |whd in ⊢ (??%); >commutative_times in ⊢(??%); @monotonic_le_times_r @Hinda
+    ]
+ ]
+qed.
+ 
+ 
+lemma lt_log2_sqrt: ∀n. 2^6 ≤ n→ log 2 n < sqrt n.
+#n #le_n >sqrt_def
+cut (0<n) [@(transitive_lt … le_n) @lt_O_S] #posn
+@true_to_le_max
+  [@le_S_S @lt_log_n_n //
+  |@le_to_leb_true 
+   cut (0<n) [@(transitive_lt … le_n) @lt_O_S] #posn
+   @(transitive_le … (le_exp_log 2 n posn))
+   <exp_2 @le_squareS_exp @true_to_le_max
+    [@(lt_to_le_to_lt … le_n) @leb_true_to_le //
+    |@le_to_leb_true //
+    ]
+  ]
+qed.
+ 
 (* monotonicity *)
 theorem monotonic_sqrt: monotonic nat le sqrt.
 #n #m #lenm >sqrt_def @true_to_le_max
-- 
2.39.2