proposition: Lemma SubSeriesCv : forall {R : ConstructiveReals} (un : nat -> CRcarrier R) (sub : SubSeq) (s : CRcarrier R), series_cv un s -> (forall n:nat, 0 <= un n) -> { t : CRcarrier R & series_cv (fun n => un (proj1_sig sub n)) t }.
proof: Proof. intros. destruct (series_cv_maj (FillSubSeqWithZeros un sub) un s) as [lim [cv _]]. - intro n. unfold FillSubSeqWithZeros. destruct (Nat.eq_dec (SubSeqInv sub n n) (S n)). rewrite CRabs_right. apply H0. apply CRle_refl. rewrite CRabs_right. apply CRle_refl. apply H0. - assumption. - exists lim. apply (CR_cv_eq _ (fun n => CRsum (FillSubSeqWithZeros un sub) (proj1_sig sub n))). induction n. + apply FillSubSeqWithZerosInit. + simpl. rewrite <- IHn. clear IHn. destruct (Nat.le_exists_sub (S (proj1_sig sub n)) (proj1_sig sub (S n))) as [p [inf _]]. destruct sub. simpl. apply l. apply le_n_S. apply Nat.le_refl. rewrite inf. rewrite Nat.add_comm. rewrite sum_assoc. apply CRplus_morph. reflexivity. rewrite Nat.add_comm. rewrite <- inf. apply eq_sym in inf. apply Nat.add_sub_eq_r in inf. subst p. apply FillSubSeqWithZerosStep. + apply (SubSeqCv _ sub lim cv). Qed.
imports: QArith PeanoNat ArithRing ConstructiveReals ConstructiveAbs ConstructiveSum ConstructivePower ConstructiveLimits