proposition: Lemma ex_series_dec (a : nat -> R) : {ex_series a} + {~ ex_series a}.
proof: Proof. case: (ex_lim_seq_dec (sum_n a)) => H. apply Lim_seq_correct in H. case: (Lim_seq (sum_n a)) H => [l | | ] H. left ; by exists l. right ; case => l H0. absurd (p_infty = Finite l) => //. rewrite -(is_lim_seq_unique _ _ H). by apply is_lim_seq_unique. right ; case => l H0. absurd (m_infty = Finite l) => //. rewrite -(is_lim_seq_unique _ _ H). by apply is_lim_seq_unique. right ; case => l. contradict H. by exists l. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Lim_seq Rbar Hierarchy