-(* the value of n could be smaller *)
-lemma k1: \forall n,p. 18 \le n \to p \le n \to 2*n/ 3 < p\to k (2*n) p = O.
-intros.unfold k.
-elim (log p (2*n))
- [reflexivity
- |rewrite > true_to_sigma_p_Sn
- [rewrite > H3.
- rewrite < plus_n_O.
- cases n1
- [rewrite < exp_n_SO.
- cut (2*n/p = 2) as H4
- [rewrite > H4.reflexivity
- |apply lt_to_le_times_to_lt_S_to_div
- [apply (ltn_to_ltO ? ? H2)
- |rewrite < sym_times.
- apply le_times_r.
- assumption
- |rewrite > sym_times in ⊢ (? ? %).
- apply lt_div_to_times
- [apply lt_O_S
- |assumption
- ]
- ]
- ]
- |cut (2*n/(p)\sup(S (S n2)) = O) as H4
- [rewrite > H4.reflexivity
- |apply lt_to_div_O.
- apply (le_to_lt_to_lt ? (exp ((2*n)/3) 2))
- [apply (le_times_to_le (exp 3 2))
- [apply leb_true_to_le.reflexivity
- |rewrite > sym_times in ⊢ (? ? %).
- rewrite > times_exp.
- apply (trans_le ? (exp n 2))
- [rewrite < assoc_times.
- rewrite > exp_SSO in ⊢ (? ? %).
- apply le_times_l.
- assumption
- |apply monotonic_exp1.
- apply (le_plus_to_le 3).
- change in ⊢ (? ? %) with ((S(2*n/3))*3).
- apply (trans_le ? (2*n))
- [simplify in ⊢ (? ? %).
- rewrite < plus_n_O.
- apply le_plus_l.
- apply (trans_le ? 18 ? ? H).
- apply leb_true_to_le.reflexivity
- |apply lt_to_le.
- apply lt_div_S.
- apply lt_O_S
- ]
- ]
- ]
- |apply (lt_to_le_to_lt ? (exp p 2))
- [apply lt_exp1
- [apply lt_O_S
- |assumption
- ]
- |apply le_exp
- [apply (ltn_to_ltO ? ? H2)
- |apply le_S_S.apply le_S_S.apply le_O_n
- ]
- ]
- ]
- ]
- ]
- |reflexivity
- ]
- ]
-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.
-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
- [apply prime_to_lt_O.apply primeb_true_to_prime.assumption
- |apply (bool_elim ? (leb (k (2*n) i) 1));intro
- [elim (le_to_or_lt_eq ? ? (leb_true_to_le ? ? H4))
- [lapply (le_S_S_to_le ? ? H5) as H6.
- apply (le_n_O_elim ? H6).
- rewrite < times_n_O.
- apply le_n
- |rewrite > (eq_to_eqb_true ? ? H5).
- rewrite > H5.apply le_n
- ]
- |apply le_O_n
- ]
- ]
- |apply (trans_le ? (pi_p (S (2*n/3)) primeb (λp:nat.(p)\sup(bool_to_nat (eqb (k (2*n) p) 1)))))
- [apply (eq_ind ? ? ? (le_n ?)).
- apply or_false_eq_SO_to_eq_pi_p
- [apply le_S_S.
- apply le_times_to_le_div2
- [apply lt_O_S
- |rewrite > sym_times in ⊢ (? ? %).
- apply le_times_n.
- apply leb_true_to_le.reflexivity
- ]
- |intros.
- unfold not_bertrand in H1.
- elim (decidable_le (S n) i)
- [left.
- apply not_prime_to_primeb_false.
- apply H1
- [assumption
- |apply le_S_S_to_le.assumption
- ]
- |right.
- rewrite > k1
- [reflexivity
- |assumption
- |apply le_S_S_to_le.
- apply not_le_to_lt.assumption
- |assumption
- ]
- ]
- ]
- |apply le_pi_p.intros.
- elim (eqb (k (2*n) i) 1)
- [rewrite < exp_n_SO.apply le_n
- |simplify.apply prime_to_lt_O.
- apply primeb_true_to_prime.
- assumption
- ]
- ]
- ]
+definition primes_below ≝ λl,n.
+ all_primes l ∧ all_below l n ∧ primes_all l n.
+
+lemma ld_to_prime: ∀i,acc. 1 < i →
+ primes_below acc i → list_divides acc i = false → prime i.
+#i #acc #posi * * #Hall #Hbelow #Hcomplete #Hfalse % //
+#m #mdivi
+cut (m ≤ i)[@divides_to_le [@lt_to_le //|//]] #lemi
+cases (le_to_or_lt_eq … lemi) [2://] #ltmi
+#lt1m @False_ind
+cut (divides (smallest_factor m) i)
+ [@(transitive_divides … mdivi) @divides_smallest_factor_n @lt_to_le //]
+#Hcut @(absurd … Hcut) @(list_divides_false … Hfalse) @Hcomplete
+ [@prime_smallest_factor_n // | @(le_to_lt_to_lt … ltmi) //]