proposition: Lemma InfiniteSum_raw_N_step : forall (fuel : nat) c (filter : Stream Q -> bool) (s : Stream Q) (q : Q), (forall p:nat, p < 2 ^ fuel -> filter (Str_nth_tl p s) = false)%nat -> InfiniteSum_raw_N fuel filter c s q = c (Str_nth_tl (2^fuel) s) (InfiniteSum_raw_N fuel filter (fun _ r => r) s q).
proof: Proof. induction fuel. - intros. simpl. unfold InfiniteSum_raw_F. destruct (filter s) eqn:des. 2: reflexivity. exfalso. specialize (H O (Nat.le_refl _)). simpl in H. rewrite H in des. discriminate. - intros. simpl. assert (forall p : nat, (p < 2 ^ fuel)%nat -> filter (Str_nth_tl p s) = false) as firstHalf. { intros. apply (H p). simpl. rewrite Nat.add_0_r. apply (Nat.lt_le_trans _ (0+2^fuel)). exact H0. apply Nat.add_le_mono_r, Nat.le_0_l. } rewrite IHfuel, IHfuel. 3: exact firstHalf. rewrite Nat.add_0_r, Str_nth_tl_plus. apply f_equal. symmetry. apply IHfuel. exact firstHalf. intros. rewrite Str_nth_tl_plus. apply H. simpl. rewrite Nat.add_0_r. apply Nat.add_lt_mono_r, 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