proposition: Lemma InfiniteSum_fat_plus : forall (fuel:nat) (filter:Stream Q -> bool) (s:Stream Q) (q : Q), InfiniteSum_fat filter s q fuel == q + InfiniteSum_fat filter s 0 fuel.
proof: Proof. induction fuel. - intros. simpl. destruct (filter s); rewrite Qplus_0_r; reflexivity. - intros. simpl. destruct (filter s). symmetry. apply Qplus_0_r. rewrite IHfuel. rewrite (IHfuel filter (tl s) (Qplus' 0 (hd s))). rewrite Qplus_assoc. apply Qplus_comp. 2: reflexivity. rewrite Qplus'_correct, Qplus'_correct, Qplus_0_l. reflexivity. 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