proposition: Lemma CauchyMorph_rat : forall {R1 R2 : ConstructiveReals} (q : Q), SlowMorph (CR_of_Q R1 q) == CR_of_Q R2 q.
proof: Proof. intros. unfold SlowMorph. destruct (CR_complete R2 _ (CRmorph_rat_cv _ (Rcv_cauchy_mod (fun n : nat => CR_of_Q R1 (let (q0, _) := CR_Q_limit (CR_of_Q R1 q) n in q0)) (CR_of_Q R1 q) (CR_Q_limit_cv (CR_of_Q R1 q))))). apply (CR_cv_unique _ _ _ c). intro p. exists (Pos.to_nat p). intros. destruct (CR_Q_limit (CR_of_Q R1 q) i). rewrite CRabs_right. - apply (CRplus_le_reg_r (CR_of_Q R2 q)). unfold CRminus. rewrite CRplus_assoc, CRplus_opp_l, CRplus_0_r, CRplus_comm. rewrite <- CR_of_Q_plus. apply CR_of_Q_le. destruct (Q_dec x0 (q + (1 # p))%Q). + destruct s. * apply Qlt_le_weak, q0. * exfalso. pose proof (CR_of_Q_lt R1 _ _ q0). apply (CRlt_asym _ _ H0). apply (CRlt_le_trans _ _ _ (snd p0)). clear H0. rewrite <- CR_of_Q_plus. apply CR_of_Q_le. apply Qplus_le_r. unfold Qle, Qnum, Qden. rewrite Z.mul_1_l, Z.mul_1_l. apply Pos2Z.pos_le_pos, Pos2Nat.inj_le. rewrite Nat2Pos.id. -- exact H. -- destruct i. ++ exfalso. inversion H. pose proof (Pos2Nat.is_pos p). rewrite H1 in H0. inversion H0. ++ discriminate. + rewrite q0. apply Qle_refl. - rewrite <- (CRplus_opp_r (CR_of_Q R2 q)). apply CRplus_le_compat_r, CR_of_Q_le. destruct (Q_dec q x0). + destruct s. * apply Qlt_le_weak, q0. * exfalso. apply (CRlt_asym _ _ (fst p0)). apply CR_of_Q_lt. exact q0. + rewrite q0. apply Qle_refl. Qed.
imports: QArith Qabs ConstructiveReals ConstructiveLimits ConstructiveAbs