proposition: Lemma InfiniteSum_raw_N_correct : forall (fuel : nat) (s : Stream Q) (filter : Stream Q -> bool) (q : Q), InfiniteSum_raw_N fuel filter (fun _ r => r) s q = InfiniteSum_fat filter s q (2 ^ fuel)%nat.
proof: Proof. induction fuel. - intros. simpl. unfold InfiniteSum_raw_F. destruct (filter s). reflexivity. simpl. destruct (filter (tl s)); reflexivity. - intros s filter q. simpl. rewrite Nat.add_0_r. destruct (decide_filter_before_n (2^fuel)%nat filter s). + destruct H as [p [H H0]]. rewrite (@InfiniteSum_fat_add_stop _ p). 3: exact H0. rewrite <- (@InfiniteSum_fat_add_stop (2^fuel)). 2: apply (Nat.le_trans _ (S p) _ (le_S _ _ (Nat.le_refl p)) H). 2: exact H0. rewrite <- IHfuel. apply (@InfiniteSum_raw_N_cont_invariant fuel p). exact H. exact H0. apply (Nat.le_trans _ (2^fuel + 0)). rewrite Nat.add_0_r. apply (Nat.le_trans _ (S p) _ (le_S _ _ (Nat.le_refl p)) H). apply Nat.add_le_mono_l, Nat.le_0_l. + rewrite InfiniteSum_fat_add_pass. 2: exact H. rewrite <- IHfuel. rewrite <- IHfuel. rewrite InfiniteSum_raw_N_step. reflexivity. exact H. 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