proposition: Lemma CR_cv_minus : forall {R : ConstructiveReals} (An Bn:nat -> CRcarrier R) (l1 l2:CRcarrier R), CR_cv R An l1 -> CR_cv R Bn l2 -> CR_cv R (fun i:nat => An i - Bn i) (l1 - l2).
proof: Proof. intros. apply CR_cv_plus. - apply H. - intros p. specialize (H0 p) as [n H0]. exists n. intros. setoid_replace (- Bn i - - l2) with (- (Bn i - l2)). + rewrite CRabs_opp. apply H0, H1. + unfold CRminus. rewrite CRopp_plus_distr, CRopp_involutive. reflexivity. Qed.
imports: QArith Qabs ConstructiveReals ConstructiveAbs