proposition: Lemma InfiniteSum_fat_add_stop : forall (p n : nat) (s : Stream Q) (filter : Stream Q -> bool) (q : Q), le n p -> filter (Str_nth_tl n s) = true -> InfiniteSum_fat filter s q p = InfiniteSum_fat filter s q n.
proof: Proof. induction p. - intros n s filter q H H0. inversion H. reflexivity. - intros n s filter q H H0. destruct n. + simpl in H0. simpl. rewrite H0. reflexivity. + specialize (IHp n (tl s) filter). simpl. destruct (filter s) eqn:des. reflexivity. rewrite IHp. reflexivity. apply le_S_n, H. exact H0. 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