proposition: Lemma SlowMorph_increasing_Qr : forall {R1 R2 : ConstructiveReals} (x : CRcarrier R1) (q : Q), CR_of_Q R1 q < x -> CR_of_Q R2 q < SlowMorph x.
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 x n in q0)) x (CR_Q_limit_cv x)))). destruct (CR_Q_dense R1 _ _ H) as [r [H0 H1]]. apply lt_CR_of_Q in H0. apply (CRlt_le_trans _ (CR_of_Q R2 r)). - apply CR_of_Q_lt, H0. - assert (forall n:nat, le O n -> CR_of_Q R2 r <= CR_of_Q R2 (let (q0, _) := CR_Q_limit x n in q0)). { intros. apply CR_of_Q_le. destruct (CR_Q_limit x n). destruct (Q_dec r x1). - destruct s. + apply Qlt_le_weak, q0. + exfalso. apply (CR_of_Q_lt R1) in q0. apply (CRlt_asym _ _ q0). exact (CRlt_trans _ _ _ H1 (fst p)). - rewrite q0. apply Qle_refl. } exact (CR_cv_bound_down _ _ _ O H2 c). Qed.
imports: QArith Qabs ConstructiveReals ConstructiveLimits ConstructiveAbs