proposition: Lemma InfiniteGeometricSum_raw_shift_prf : forall (s : Stream Q) (n : nat) {a : Q} (Gs : GeometricSeries a (Str_nth_tl n s)), 0 <= a -> a < 1 -> is_RegularFunction Qball (InfiniteGeometricSum_shift_raw s n Gs).
proof: Proof. intros. intros e1 e2. apply AbsSmall_Qabs. unfold InfiniteGeometricSum_shift_raw. setoid_replace (take s n Qplus' 0 + InfiniteGeometricSum_raw a (Str_nth_tl n s) e1 - (take s n Qplus' 0 + InfiniteGeometricSum_raw a (Str_nth_tl n s) e2)) with (InfiniteGeometricSum_raw a (Str_nth_tl n s) e1 - InfiniteGeometricSum_raw a (Str_nth_tl n s) e2) by (unfold canonical_names.equiv, stdlib_rationals.Q_eq; ring). apply AbsSmall_Qabs. apply (InfiniteGeometricSum_raw_prf H H0 Gs). 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