proposition: Lemma Un_cv_nat_real : forall {R : ConstructiveReals} (un : nat -> CRcarrier R) (l : CRcarrier R), CR_cv R un l -> forall eps : CRcarrier R, 0 < eps -> { p : nat & forall i:nat, le p i -> CRabs R (un i - l) < eps }.
proof: Proof. intros. destruct (CR_archimedean R (CRinv R eps (inr H0))) as [k kmaj]. assert (0 < CR_of_Q R (Z.pos k # 1)). { apply CR_of_Q_lt. reflexivity. } specialize (H k) as [p pmaj]. exists p. intros. apply (CRle_lt_trans _ (CR_of_Q R (1 # k))). - apply pmaj, H. - apply (CRmult_lt_reg_l (CR_of_Q R (Z.pos k # 1))). + exact H1. + rewrite <- CR_of_Q_mult. apply (CRle_lt_trans _ 1). * apply CR_of_Q_le. unfold Qle; simpl. do 2 rewrite Pos.mul_1_r. apply Z.le_refl. * apply (CRmult_lt_reg_r (CRinv R eps (inr H0))). -- apply CRinv_0_lt_compat, H0. -- rewrite CRmult_1_l, CRmult_assoc. rewrite CRinv_r, CRmult_1_r. exact kmaj. Qed.
imports: QArith Qabs ConstructiveReals ConstructiveAbs