proposition: Lemma CR_cv_abs_cont : forall {R : ConstructiveReals} (u : nat -> CRcarrier R) (s : CRcarrier R), CR_cv R u s -> CR_cv R (fun n => CRabs R (u n)) (CRabs R s).
proof: Proof. intros. intros eps. specialize (H eps) as [N lim]. exists N. intros n H. apply (CRle_trans _ (CRabs R (u n - s))). - apply CRabs_triang_inv2. - apply lim. assumption. Qed.
imports: QArith Qabs ConstructiveReals ConstructiveAbs