proposition: Lemma InfiniteSum_raw_N_extend : forall (p q:nat) s (err : Stream Q -> bool) (r:Q), (Is_true (err (Str_nth_tl (2^p) s))) -> (p <= q)%nat -> InfiniteSum_raw_N p err (fun _ r => r) s r = InfiniteSum_raw_N q err (fun _ r => r) s r.
proof: Proof. intros. rewrite InfiniteSum_raw_N_correct, InfiniteSum_raw_N_correct. symmetry. apply InfiniteSum_fat_add_stop. apply Nat.pow_le_mono_r. discriminate. exact H0. unfold Is_true in H. destruct (err (Str_nth_tl (2 ^ p) s)). reflexivity. contradiction. 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