proposition: Lemma CR_cv_bound_down : forall {R : ConstructiveReals} (u : nat -> CRcarrier R) (A l : CRcarrier R) (N : nat), (forall n:nat, le N n -> A <= u n) -> CR_cv R u l -> A <= l.
proof: Proof. intros. intro r. apply (CRplus_lt_compat_r (-l)) in r. rewrite CRplus_opp_r in r. destruct (Un_cv_nat_real _ l H0 (A - l) r) as [n H1]. apply (H (n+N)%nat). - rewrite <- (Nat.add_0_l N), Nat.add_assoc. apply Nat.add_le_mono_r, Nat.le_0_l. - specialize (H1 (n+N)%nat). apply (CRplus_lt_reg_r (-l)). assert (n + N >= n)%nat. + rewrite <- (Nat.add_0_r n), <- Nat.add_assoc. apply Nat.add_le_mono_l, Nat.le_0_l. + specialize (H1 H2). apply (CRle_lt_trans _ (CRabs R (u (n + N)%nat - l))). * apply CRle_abs. * assumption. Qed.
imports: QArith Qabs ConstructiveReals ConstructiveAbs