proposition: Lemma ex_finite_lim_seq_incr (u : nat -> R) (M : R) : (forall n, (u n) <= (u (S n))) -> (forall n, u n <= M) -> ex_finite_lim_seq u.
proof: Proof. intros. case: (ex_finite_lim_seq_decr (fun n => - u n) (- M)). move => n ; by apply Ropp_le_contravar. move => n ; by apply Ropp_le_contravar. move => l ; move => Hu. exists (- l). apply is_lim_seq_spec in Hu. apply is_lim_seq_spec. intros eps. case: (Hu eps) => {Hu} N Hu. exists N => n Hn. replace (u n - - l) with (-(- u n - l)) by ring. rewrite Rabs_Ropp ; by apply Hu. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lub Markov Hierarchy