Bolzano & Weierstrassの定理(有界な数列は収束する部分列を持つ)

Bolzano Weierstrass の定理はCoqではもう既に証明されていて、しかもそれは標準ライブラリに備わっている！
Rtopology.vというライブラリのソースを見ればこの定理を見つけることができる。

Theorem Bolzano_Weierstrass :
  forall (un:nat -> R) (X:R -> Prop),
    compact X -> (forall n:nat, X (un n)) ->  exists l : R, ValAdh un l.

実数列unは nat -> R 型で、領域 X ⊂ R はR -> Prop 型で表現しているようだ。

ValAdh un lの定義は以下のとおりで、lに収束するunの部分列が存在することと同等の命題みたいだ。

Definition ValAdh (un:nat -> R) (x:R) : Prop :=
  forall (V:R -> Prop) (N:nat),
    neighbourhood V x ->  exists p : nat, (N <= p)%nat /\ V (un p).