proposition: Lemma growing_ineq : forall (Un:nat -> R) (l:R), Un_growing Un -> Un_cv Un l -> forall n:nat, Un n <= l.
proof: Proof. intros; destruct (total_order_T (Un n) l) as [[Hlt|Heq]|Hgt]. - left; assumption. - right; assumption. - cut (0 < Un n - l). + intro; unfold Un_cv in H0; unfold Rdist in H0. elim (H0 (Un n - l) H1); intros N1 H2. set (N := max n N1). cut (Un n - l <= Un N - l). * intro; cut (Un N - l < Un n - l). -- intro; elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H3 H4)). -- apply Rle_lt_trans with (Rabs (Un N - l)). ++ apply RRle_abs. ++ apply H2. unfold ge, N; apply Nat.le_max_r. * unfold Rminus; do 2 rewrite <- (Rplus_comm (- l)); apply Rplus_le_compat_l. apply tech9. -- assumption. -- unfold N; apply Nat.le_max_l. + apply Rplus_lt_reg_l with l. rewrite Rplus_0_r. replace (l + (Un n - l)) with (Un n); [ assumption | ring ]. Qed.
imports: Rbase Rfunctions Rseries Lia