proposition: Lemma AltSeries_raw_prf : forall x cvmod, Str_alt_decr x -> Limit_zero x cvmod -> is_RegularFunction Qball (AltSeries_raw x cvmod).
proof: Proof. intros x cvmod decr lz ε1 ε2. apply AltSeries_further. exact decr. apply lz. apply lz. apply Qle_refl. apply Qle_refl. Qed.
imports: Coq.setoid_ring.ArithRing Coq.Bool.Bool Coq.QArith.Qpower Coq.QArith.Qabs CoRN.algebra.RSetoid CoRN.metric2.Metric CoRN.metric2.UniformContinuity CoRN.reals.fast.CRArith CoRN.model.metric2.Qmetric CoRN.reals.fast.LazyNat CoRN.reals.fast.CRstreams CoRN.metric2.Limit CoRN.model.totalorder.QposMinMax CoRN.classes.Qclasses MathClasses.interfaces.abstract_algebra