proposition: Lemma CR_Q_limit_cv : forall {R : ConstructiveReals} (x : CRcarrier R), CR_cv R (fun n => CR_of_Q R (let (q,_) := CR_Q_limit x n in q)) x.
proof: Proof. intros R x p. exists (Pos.to_nat p). intros. destruct (CR_Q_limit x i). rewrite CRabs_right. - apply (CRplus_le_reg_r x). unfold CRminus. rewrite CRplus_assoc, CRplus_opp_l, CRplus_0_r, CRplus_comm. apply (CRle_trans _ (x + CR_of_Q R (1 # Pos.of_nat i))). + apply CRlt_asym, p0. + apply CRplus_le_compat_l, CR_of_Q_le. 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 <- (CRplus_opp_r x). apply CRplus_le_compat_r, CRlt_asym, p0. Qed.
imports: QArith Qabs ConstructiveReals ConstructiveLimits ConstructiveAbs