proposition: Lemma InfiniteSum_fat_wd : forall (fuel:nat) (filter:Stream Q -> bool) (s:Stream Q) (q r : Q), q == r -> InfiniteSum_fat filter s q fuel == InfiniteSum_fat filter s r fuel.
proof: Proof. induction fuel. - intros. simpl. destruct (filter s); exact H. - intros. simpl. destruct (filter s). exact H. apply IHfuel. rewrite Qplus'_correct, Qplus'_correct. apply Qplus_comp. exact H. 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