proposition: Lemma InfiniteSum_fat_extend : forall (n : nat) (s : Stream Q) (filter : Stream Q -> bool) (q : Q), filter (Str_nth_tl n s) = true -> InfiniteSum_fat filter s q n = InfiniteSum_fat filter s q (S n).
proof: Proof. intros. symmetry. apply InfiniteSum_fat_add_stop. apply le_S, Nat.le_refl. exact H. Qed.
imports: CoRN.metric2.Metric CoRN.metric2.UniformContinuity CoRN.reals.fast.CRAlternatingSum CoRN.reals.fast.CRstreams CoRN.model.totalorder.QposMinMax CoRN.model.totalorder.QMinMax Coq.QArith.Qpower Coq.QArith.Qabs Coq.ZArith.Zdiv