proposition: Lemma SlowMorph_increasing_Ql : forall {R1 R2 : ConstructiveReals} (x : CRcarrier R1) (q : Q), x < CR_of_Q R1 q -> SlowMorph x < 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 x n in q0)) x (CR_Q_limit_cv x)))). assert (CR_cv R1 (fun n => CR_of_Q R1 (let (q0, _) := CR_Q_limit x n in q0) + CR_of_Q R1 (1 # Pos.of_nat n)) x). { apply (CR_cv_proper _ (x+0)). - apply CR_cv_plus. + apply CR_Q_limit_cv. + intro p. exists (Pos.to_nat p). intros. unfold CRminus. rewrite CRopp_0, CRplus_0_r. rewrite CRabs_right. * apply CR_of_Q_le. unfold Qle, Qnum, Qden. do 2 rewrite Z.mul_1_l. apply Pos2Z.pos_le_pos, Pos2Nat.inj_le. rewrite Nat2Pos.id. -- exact H0. -- destruct i. ++ inversion H0. pose proof (Pos2Nat.is_pos p). rewrite H2 in H1. inversion H1. ++ discriminate. * apply CR_of_Q_le. discriminate. - rewrite CRplus_0_r. reflexivity. } pose proof (CR_cv_open_above _ _ _ H0 H) as [n nmaj]. apply (CRle_lt_trans _ (CR_of_Q R2 (let (q0, _) := CR_Q_limit x n in q0 + (1 # Pos.of_nat n)))). - apply (CR_cv_bound_up (fun n : nat => CR_of_Q R2 (let (q0, _) := CR_Q_limit x n in q0)) _ _ n). 2: exact c. intros. destruct (CR_Q_limit x n0), (CR_Q_limit x n). apply CR_of_Q_le, Qlt_le_weak. apply (lt_CR_of_Q R1). apply (CRlt_le_trans _ _ _ (snd p)). apply (CRle_trans _ (CR_of_Q R1 x2 + CR_of_Q R1 (1 # Pos.of_nat n0))). + apply CRplus_le_compat_r. apply CRlt_asym, p0. + rewrite <- CR_of_Q_plus. apply CR_of_Q_le. apply Qplus_le_r. unfold Qle, Qnum, Qden. do 2 rewrite Z.mul_1_l. apply Pos2Z.pos_le_pos, Pos2Nat.inj_le. destruct n. * destruct n0. -- apply Nat.le_refl. -- rewrite (Nat2Pos.id (S n0)). ++ apply -> Nat.succ_le_mono; apply Nat.le_0_l. ++ discriminate. * destruct n0. -- exfalso; inversion H1. -- rewrite Nat2Pos.id, Nat2Pos.id. ++ exact H1. ++ discriminate. ++ discriminate. - specialize (nmaj n (Nat.le_refl n)). destruct (CR_Q_limit x n). apply CR_of_Q_lt. rewrite <- CR_of_Q_plus in nmaj. apply lt_CR_of_Q in nmaj. exact nmaj. Qed.
imports: QArith Qabs ConstructiveReals ConstructiveLimits ConstructiveAbs