Require Import Reals.
Require Import Fourier.

Open Scope R_scope.

Theorem R_uncountable_strong :
  ∀ (f : nat → R) (x y : R), x < y → {l : R | ∀ n, l ≠ f n & x ≤ l ≤ y}.
Proof.
intros f x y H.
pose (lf := l x y H f).
∃ lf.
  intros n Hc; destruct (l_not_in_Rn x y H f n); unfold Rn; auto.
  apply l_in_segment.
Qed.

Theorem R_uncountable : ∀ (f : nat → R), {l : R | ∀ n, l ≠ f n}.
Proof.
apply (segment_uncountable 0 1); fourier.
Qed.