proposition: Lemma CR_cv_dist_cont : forall {R : ConstructiveReals} (u : nat -> CRcarrier R) (a s : CRcarrier R), CR_cv R u s -> CR_cv R (fun n => CRabs R (a - u n)) (CRabs R (a - s)).
proof: Proof. intros. apply CR_cv_abs_cont. intros eps. specialize (H eps) as [N lim]. exists N. intros n H. setoid_replace (a - u n - (a - s)) with (s - (u n)). - specialize (lim n). rewrite CRabs_minus_sym. apply lim. assumption. - unfold CRminus. rewrite CRopp_plus_distr, CRopp_involutive. rewrite (CRplus_comm a), (CRplus_comm s). rewrite CRplus_assoc. apply CRplus_morph. + reflexivity. + rewrite <- CRplus_assoc, CRplus_opp_r, CRplus_0_l. reflexivity. Qed.
imports: QArith Qabs ConstructiveReals ConstructiveAbs