-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