proposition: Lemma ex_lim_seq_incr (u : nat -> R) : (forall n, (u n) <= (u (S n))) -> ex_lim_seq u.
proof: Proof. move => H. exists (Sup_seq u). apply is_lim_seq_spec. rewrite /Sup_seq ; case: ex_sup_seq ; case => [l | | ] //= Hl. move => eps ; case: (Hl eps) => Hl1 [N Hl2]. exists N => n Hn. apply Rabs_lt_between' ; split. apply Rlt_le_trans with (1 := Hl2). elim: Hn => [ | {} n Hn IH]. by apply Rle_refl. apply Rle_trans with (1 := IH). by apply H. by apply Hl1. move => M. case: (Hl M) => {Hl} N Hl. exists N => n Hn. apply Rlt_le_trans with (1 := Hl). elim: Hn => [ | {} n Hn IH]. by apply Rle_refl. apply Rle_trans with (1 := IH). by apply H. move => M ; exists O => n Hn ; by apply Hl. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lub Markov Hierarchy