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