-theorem exp_plus_SSO: \forall a,b. exp (a+b) 2 = (exp a 2) + 2*a*b + (exp b 2).
-intros.
-rewrite > exp_SSO.
-rewrite > distr_times_plus.
-rewrite > times_plus_l.
-rewrite < exp_SSO.
-rewrite > assoc_plus.
-rewrite > assoc_plus.
-apply eq_f.
-rewrite > times_plus_l.
-rewrite < exp_SSO.
-rewrite < assoc_plus.
-rewrite < sym_times.
-rewrite > plus_n_O in ⊢ (? ? (? (? ? %) ?) ?).
-rewrite > assoc_times.
-apply eq_f2;reflexivity.
-qed.
-
-theorem tech3: \forall n. (exp 2 8) \le n \to 2*(S(log 2 (2*n))) \le sqrt (2*n).
-intros.
-lapply (le_log 2 ? ? (le_n ?) H) as H1.
-rewrite > exp_n_SO in ⊢ (? (? ? (? (? ? (? % ?)))) ?).
-rewrite > log_exp
- [rewrite > sym_plus.
- rewrite > plus_n_Sm.
- unfold sqrt.
- apply f_m_to_le_max
- [apply le_times_r.
- apply (trans_le ? (2*log 2 n))
- [rewrite < times_SSO_n.
- apply le_plus_r.
- apply (trans_le ? 8)
- [apply leb_true_to_le.reflexivity
- |rewrite < (eq_log_exp 2)
- [assumption
- |apply le_n
- ]
- ]
- |apply (trans_le ? ? ? ? (le_exp_log 2 ? ? )).
- apply le_times_SSO_n_exp_SSO_n.
- apply (lt_to_le_to_lt ? ? ? ? H).
- apply leb_true_to_le.reflexivity
- ]
- |apply le_to_leb_true.
- rewrite > assoc_times.
- apply le_times_r.
- rewrite > sym_times.
- rewrite > assoc_times.
- rewrite < exp_SSO.
- rewrite > exp_plus_SSO.
- rewrite > distr_times_plus.
- rewrite > distr_times_plus.
- rewrite > assoc_plus.
- apply (trans_le ? (4*exp (log 2 n) 2))
- [change in ⊢ (? ? (? % ?)) with (2*2).
- rewrite > assoc_times in ⊢ (? ? %).
- rewrite < times_SSO_n in ⊢ (? ? %).
- apply le_plus_r.
- rewrite < times_SSO_n in ⊢ (? ? %).
- apply le_plus
- [rewrite > sym_times in ⊢ (? (? ? %) ?).
- rewrite < assoc_times.
- rewrite < assoc_times.
- change in ⊢ (? (? % ?) ?) with 8.
- rewrite > exp_SSO.
- apply le_times_l.
- (* strange things here *)
- rewrite < (eq_log_exp 2)
- [assumption
- |apply le_n
- ]
- |apply (trans_le ? (log 2 n))
- [change in ⊢ (? % ?) with 8.
- rewrite < (eq_log_exp 2)
- [assumption
- |apply le_n
- ]
- |rewrite > exp_n_SO in ⊢ (? % ?).
- apply le_exp
- [apply lt_O_log
- [apply (lt_to_le_to_lt ? ? ? ? H).
- apply leb_true_to_le.reflexivity
- |apply (lt_to_le_to_lt ? ? ? ? H).
- apply leb_true_to_le.reflexivity
- ]
- |apply le_n_Sn
- ]
- ]
- ]
- |change in ⊢ (? (? % ?) ?) with (exp 2 2).
- apply (trans_le ? ? ? ? (le_exp_log 2 ? ?))
- [apply le_times_exp_n_SSO_exp_SSO_n
- [apply le_n
- |change in ⊢ (? % ?) with 8.
- rewrite < (eq_log_exp 2)
- [assumption
- |apply le_n
- ]
- ]
- |apply (lt_to_le_to_lt ? ? ? ? H).
- apply leb_true_to_le.reflexivity
- ]
- ]
- ]
- |apply le_n
- |apply (lt_to_le_to_lt ? ? ? ? H).
- apply leb_true_to_le.reflexivity
- ]
-qed.
-
-theorem le_to_bertrand2:
-\forall n. (exp 2 8) \le n \to bertrand n.
-intros.
-apply not_not_bertrand_to_bertrand.unfold.intro.
-absurd (2*n / 3 \le (sqrt(2*n)/2)*S(log 2 (2*n)))
- [apply not_bertrand_to_le2
- [apply (trans_le ? ? ? ? H).
- apply le_exp
- [apply lt_O_S
- |apply le_n_Sn
- ]
- |assumption
- ]
- |apply lt_to_not_le.
- apply (le_to_lt_to_lt ? ? ? ? (lt_div_S_div ? ? ? ?))
- [apply tech.apply tech3.assumption
- |apply lt_O_S
- |apply (trans_le ? (2*exp 2 8))
- [apply leb_true_to_le.reflexivity
- |apply le_times_r.assumption
+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
+@(primes_below_to_bertrand (S it) (list_of_primes it) … posn)
+ [@primeb_true_to_prime >itdef %
+ |>(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] *
+ [#eqp2 @False_ind @(absurd ? lt2p) @le_to_not_lt >eqp2 @le_n
+ |#H @H