proposition: Lemma Un_cv_real_nat : forall {R : ConstructiveReals} (un : nat -> CRcarrier R) (l : CRcarrier R), (forall eps : CRcarrier R, 0 < eps -> { p : nat & forall i:nat, le p i -> CRabs R (un i - l) < eps }) -> CR_cv R un l.
proof: Proof. intros. intros n. specialize (H (CR_of_Q R (1#n))) as [p pmaj]. - apply CR_of_Q_lt. reflexivity. - exists p. intros. apply CRlt_asym. apply pmaj. apply H. Qed.
imports: QArith Qabs ConstructiveReals ConstructiveAbs