proposition: Lemma mult_Streams_Gs : forall a (x y : Stream Q), (DecreasingNonNegative x) -> (GeometricSeries a y) -> (GeometricSeries a (mult_Streams x y)).
proof: Proof. cofix mult_Streams_Gs. intros a x y Hx Hy. constructor. destruct Hy as [Hy _]. apply dnn_alt in Hx. destruct Hx as [[[Hx2 _] [[Hx0 Hx1] _]] _]. simpl. rewrite -> Qabs_Qmult. apply Qle_trans with (Qabs (CoqStreams.hd x) * Qabs (CoqStreams.hd (CoqStreams.tl y))). apply Qmult_le_compat_r. do 2 (rewrite -> Qabs_pos; try assumption). apply Qabs_nonneg. rewrite -> Qabs_Qmult. rewrite Qmult_comm. rewrite (Qmult_comm (Qabs (CoqStreams.hd x))), Qmult_assoc. apply Qmult_le_compat_r; try assumption. apply Qabs_nonneg. destruct Hy. apply mult_Streams_Gs. 2: exact Hy. apply Hx. 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