proposition: Lemma InfiniteSum_fat_minus : forall (i p : nat) (s : Stream Q) (q : Q), InfiniteSum_fat (fun _ => false) s q (p + i) - InfiniteSum_fat (fun _ => false) s q i == InfiniteSum_fat (fun _ => false) (Str_nth_tl i s) 0 p.
proof: Proof. induction i. - intros. simpl. rewrite Nat.add_0_r. unfold Qminus. rewrite InfiniteSum_fat_plus. ring. - intros. rewrite Nat.add_succ_r. simpl. rewrite IHi. 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