proposition: Lemma powers_help_Gs (a : Q) : (0 <= a) -> forall c, (GeometricSeries a (powers_help a c)).
proof: Proof. intros Ha. cofix powers_help_Gs. intros c. constructor. simpl. rewrite -> Qmult_comm. rewrite -> Qabs_Qmult. rewrite -> (Qabs_pos a); try assumption. apply Qle_refl. apply powers_help_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