proposition: Lemma ex_lim_seq_dec (u : nat -> R) : {ex_lim_seq u} + {~ex_lim_seq u}.
proof: Proof. case: (Rbar_eq_dec (LimSup_seq u) (LimInf_seq u)) => H. left ; by apply ex_lim_LimSup_LimInf_seq. right ; contradict H ; by apply ex_lim_LimSup_LimInf_seq. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lub Markov Hierarchy