proposition: Lemma ex_finite_lim_seq_dec (u : nat -> R) : {ex_finite_lim_seq u} + {~ ex_finite_lim_seq u}.
proof: Proof. case: (ex_lim_seq_dec u) => H. apply Lim_seq_correct in H. case: (Lim_seq u) H => [l | | ] H. left ; by exists l. right ; rewrite ex_finite_lim_seq_correct. rewrite (is_lim_seq_unique _ _ H) /is_finite //= ; by case. right ; rewrite ex_finite_lim_seq_correct. rewrite (is_lim_seq_unique _ _ H) /is_finite //= ; by case. right ; rewrite ex_finite_lim_seq_correct. contradict H ; by apply H. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lub Markov Hierarchy