proposition: Lemma CR_cv_bound_up : forall {R : ConstructiveReals} (u : nat -> CRcarrier R) (A l : CRcarrier R) (N : nat), (forall n:nat, le N n -> u n <= A) -> CR_cv R u l -> l <= A.
proof: Proof. intros. intro r. apply (CRplus_lt_compat_r (-A)) in r. rewrite CRplus_opp_r in r. destruct (Un_cv_nat_real _ l H0 (l-A) r) as [n H1]. apply (H (n+N)%nat). - rewrite <- (Nat.add_0_l N). apply Nat.add_le_mono_r, Nat.le_0_l. - specialize (H1 (n+N)%nat). apply (CRplus_lt_reg_l R (l - A - u (n+N)%nat)). unfold CRminus. repeat rewrite CRplus_assoc. rewrite CRplus_opp_l, CRplus_0_r, (CRplus_comm (-A)). rewrite CRplus_assoc, CRplus_opp_r, CRplus_0_r. apply (CRle_lt_trans _ _ _ (CRle_abs _)). fold (l - u (n+N)%nat). rewrite CRabs_minus_sym. apply H1. rewrite <- (Nat.add_0_r n), <- Nat.add_assoc. apply Nat.add_le_mono_l, Nat.le_0_l. Qed.
imports: QArith Qabs ConstructiveReals ConstructiveAbs