proposition: Lemma CRmorph_rat_cv : forall {R1 R2 : ConstructiveReals} (qn : nat -> Q), CR_cauchy R1 (fun n => CR_of_Q R1 (qn n)) -> CR_cauchy R2 (fun n => CR_of_Q R2 (qn n)).
proof: Proof. intros. intro p. destruct (H p) as [n nmaj]. exists n. intros. specialize (nmaj i j H0 H1). unfold CRminus. rewrite <- CR_of_Q_opp, <- CR_of_Q_plus, CR_of_Q_abs. unfold CRminus in nmaj. rewrite <- CR_of_Q_opp, <- CR_of_Q_plus, CR_of_Q_abs in nmaj. apply CR_of_Q_le. destruct (Q_dec (Qabs (qn i + - qn j)) (1#p)). - destruct s. + apply Qlt_le_weak, q. + exfalso. apply (Qlt_not_le _ _ q). apply (CR_of_Q_lt R1) in q. contradiction. - rewrite q. apply Qle_refl. Qed.
imports: QArith Qabs ConstructiveReals ConstructiveLimits ConstructiveAbs