proposition: Lemma InfiniteSum_fat_remove_filter : forall (fuel:nat) (filter:Stream Q -> bool) (s:Stream Q) (q : Q), filter (Str_nth_tl fuel s) = true -> exists n:nat, InfiniteSum_fat filter s q fuel = InfiniteSum_fat (fun _ => false) s q n /\ (forall p:nat, lt p n -> filter (Str_nth_tl p s) = false) /\ filter (Str_nth_tl n s) = true.
proof: Proof. induction fuel. - intros. exists O. split. 2: split. simpl. destruct (filter s); reflexivity. intros. exfalso; inversion H0. exact H. - intros. destruct (filter s) eqn:des. + exists O. split. 2: split. simpl. rewrite des. reflexivity. intros. exfalso; inversion H0. exact des. + specialize (IHfuel filter (tl s) (Qplus' q (hd s)) H) as [n [H1 H2]]. exists (S n). split. 2: split. simpl. rewrite des. rewrite H1. reflexivity. intros. destruct p. exact des. simpl. apply H2. apply le_S_n in H0. exact H0. apply H2. 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