proposition: Lemma is_lim_seq_decr_compare (u : nat -> R) (l : R) : is_lim_seq u l -> (forall n, (u (S n)) <= (u n)) -> forall n, l <= u n.
proof: Proof. move /is_lim_seq_spec => Hu H n. apply Rnot_lt_le => H0. apply Rminus_lt_0 in H0. case: (Hu (mkposreal _ H0)) => {Hu} /= Nu Hu. move: (Hu _ (MyNat.le_add_l Nu n)). apply Rle_not_lt. apply Rle_trans with (2 := Rabs_maj2 _). rewrite Ropp_minus_distr'. apply Rplus_le_compat_l. apply Ropp_le_contravar. elim: (Nu) => [ | m IH]. rewrite Nat.add_0_r ; by apply Rle_refl. rewrite -plus_n_Sm. apply Rle_trans with (2 := IH). by apply H. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lub Markov Hierarchy