| cons h2 t2 => (andb (checker t1) (leb h1 (2*h2))) ]].
lemma checker_cons : \forall t,l.checker (t::l) = true \to checker l = true.
-intros 2;simplify;intro;generalize in match H;elim l
+intros 2;simplify;intro;elim l in H ⊢ %
[reflexivity
- |change in H2 with (andb (checker (a::l1)) (leb t (a+(a+O))) = true);
- apply (andb_true_true ? ? H2)]
+ |change in H1 with (andb (checker (a::l1)) (leb t (a+(a+O))) = true);
+ apply (andb_true_true ? ? H1)]
qed.
theorem checker_sound : \forall l1,l2,l,x,y.l = l1@(x::y::l2) \to
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.
+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