proposition: Lemma CR_cv_plus : forall {R : ConstructiveReals} (xn yn : nat -> CRcarrier R) (a b : CRcarrier R), CR_cv R xn a -> CR_cv R yn b -> CR_cv R (fun n => xn n + yn n) (a + b).
proof: Proof. intros. intro p. specialize (H (2*p)%positive) as [i imaj]. specialize (H0 (2*p)%positive) as [j jmaj]. exists (max i j). intros. apply (CRle_trans _ (CRabs R (CRplus R (CRminus R (xn i0) a) (CRminus R (yn i0) b)))). - apply CRabs_morph. unfold CRminus. do 2 rewrite <- (Radd_assoc (CRisRing R)). apply CRplus_morph. + reflexivity. + rewrite CRopp_plus_distr. destruct (CRisRing R). rewrite Radd_comm, <- Radd_assoc. apply CRplus_morph. * reflexivity. * rewrite Radd_comm. reflexivity. - apply (CRle_trans _ _ _ (CRabs_triang _ _)). apply (CRle_trans _ (CRplus R (CR_of_Q R (1 # 2*p)) (CR_of_Q R (1 # 2*p)))). + apply CRplus_le_compat. * apply imaj, (Nat.le_trans _ _ _ (Nat.le_max_l _ _) H). * apply jmaj, (Nat.le_trans _ _ _ (Nat.le_max_r _ _) H). + apply (CRle_trans _ (CR_of_Q R ((1 # 2 * p) + (1 # 2 * p)))). * apply CR_of_Q_plus. * apply CR_of_Q_le. rewrite Qinv_plus_distr. setoid_replace (1 + 1 # 2 * p) with (1 # p). -- apply Qle_refl. -- reflexivity. Qed.
imports: QArith Qabs ConstructiveReals ConstructiveAbs