proposition: Lemma Rcv_cauchy_mod : forall {R : ConstructiveReals} (un : nat -> CRcarrier R) (l : CRcarrier R), CR_cv R un l -> CR_cauchy R un.
proof: Proof. intros. intros p. specialize (H (2*p)%positive) as [k H]. exists k. intros n q H0 H1. setoid_replace (1#p)%Q with ((1#2*p) + (1#2*p))%Q. - rewrite CR_of_Q_plus. setoid_replace (un n - un q) with ((un n - l) - (un q - l)). + apply (CRle_trans _ _ _ (CRabs_triang _ _)). apply CRplus_le_compat. * apply H, H0. * rewrite CRabs_opp. apply H. apply H1. + unfold CRminus. rewrite CRplus_assoc. apply CRplus_morph. * reflexivity. * rewrite CRplus_comm, CRopp_plus_distr, CRopp_involutive. rewrite CRplus_assoc, CRplus_opp_r, CRplus_0_r. reflexivity. - rewrite Qinv_plus_distr. reflexivity. Qed.
imports: QArith Qabs ConstructiveReals ConstructiveAbs