proposition: Lemma growing_ineq : forall {R : ConstructiveReals} (Un:nat -> CRcarrier R) (l:CRcarrier R), (forall n:nat, Un n <= Un (S n)) -> CR_cv R Un l -> forall n:nat, Un n <= l.
proof: Proof. intros. intro abs. destruct (Un_cv_nat_real _ l H0 (Un n - l)) as [N H1]. - rewrite <- (CRplus_opp_r l). apply CRplus_lt_compat_r. exact abs. - specialize (H1 (max n N) (Nat.le_max_r _ _)). apply (CRle_lt_trans _ _ _ (CRle_abs _)) in H1. apply CRplus_lt_reg_r in H1. apply (CR_growing_transit Un H n (max n N)). + apply Nat.le_max_l. + exact H1. Qed.
imports: QArith Qabs ConstructiveReals ConstructiveAbs