proposition: Lemma SubSeqCv : forall {R : ConstructiveReals} (un : nat -> CRcarrier R) (sub : SubSeq) (l : CRcarrier R), CR_cv R un l -> CR_cv R (fun n => un (proj1_sig sub n)) l.
proof: Proof. intros. intros p. specialize (H p) as [N cv]. exists N. intros. apply cv. apply (Nat.le_trans _ i). assumption. apply SubSeqAboveId. Qed.
imports: QArith PeanoNat ArithRing ConstructiveReals ConstructiveAbs ConstructiveSum ConstructivePower ConstructiveLimits