proposition: Theorem R_uncountable_strong : forall (f : nat -> R) (x y : R), x < y -> {l : R | forall n, l <> f n & x <= l <= y}.
proof: Proof. intros f x y H. pose (lf := l x y H f). exists lf. intros n Hc; destruct (l_not_in_Rn x y H f n); unfold Rn; auto. apply l_in_segment. Qed.
imports: Reals Lra