proposition: Lemma ex_finite_lim_seq_decr (u : nat -> R) (M : R) : (forall n, (u (S n)) <= (u n)) -> (forall n, M <= u n) -> ex_finite_lim_seq u.
proof: Proof. intros. apply ex_finite_lim_seq_correct. have H1 : ex_lim_seq u. exists (real (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: (Hl (u O) O) => H1 ; by apply Rlt_irrefl in H1. case: (Hl M) => {Hl} n Hl. apply Rlt_not_le in Hl. by move: (Hl (H0 n)). split => //. apply Lim_seq_correct in H1. case: (Lim_seq u) H1 => [l | | ] /= Hu. by []. apply is_lim_seq_spec in Hu. case: (Hu (u O)) => {Hu} N Hu. move: (Hu N (Nat.le_refl _)) => {} Hu. contradict Hu ; apply Rle_not_lt. elim: N => [ | N IH]. by apply Rle_refl. by apply Rle_trans with (1 := H _). apply is_lim_seq_spec in Hu. case: (Hu M) => {Hu} N Hu. move: (Hu N (Nat.le_refl _)) => {} Hu. contradict Hu ; by apply Rle_not_lt. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lub Markov Hierarchy