proposition: Lemma CR_cv_opp : forall {R : ConstructiveReals} (xn : nat -> CRcarrier R) (l : CRcarrier R), CR_cv R xn l -> CR_cv R (fun n => - xn n) (- l).
proof: Proof. intros. intro p. specialize (H p) as [n nmaj]. exists n. intros. specialize (nmaj i H). apply (CRle_trans _ (CRabs R (CRminus R (xn i) l))). 2: exact nmaj. clear nmaj H. unfold CRminus. rewrite <- CRopp_plus_distr, CRabs_opp. apply CRle_refl. Qed.
imports: QArith Qabs ConstructiveReals ConstructiveAbs