proposition: Lemma powers_Gs (a : Q) : (0 <= a) -> (GeometricSeries a (powers a)).
proof: Proof. intros Ha. apply (powers_help_Gs Ha). 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