proposition: Lemma InfiniteSum_fat_add_pass : forall (n p : nat) (s : Stream Q) (filter : Stream Q -> bool) (q : Q), (forall k:nat, lt k n -> filter (Str_nth_tl k s) = false) -> InfiniteSum_fat filter s q (n+p) = InfiniteSum_fat filter (Str_nth_tl n s) (InfiniteSum_fat filter s q n) p.
proof: Proof. induction n. - intros. simpl. destruct (filter s); reflexivity. - intros. pose proof (H O (le_n_S 0 n (Nat.le_0_l _))) as zeroFalse. simpl in zeroFalse. simpl. rewrite zeroFalse. rewrite IHn. reflexivity. intros k H0. destruct n. exfalso; inversion H0. apply Nat.le_succ_r in H0. destruct H0. apply (H (S k)), le_n_S, le_S, H0. inversion H0. subst k. apply (H (S n) (Nat.le_refl _)). 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