proposition: Lemma powers_help_dnn : forall x, (0 <= x) -> DecreasingNonNegative (powers_help a x).
proof: Proof. intros x Hx. destruct Ha as [Ha0 Ha1]. generalize x Hx; clear x Hx. cofix powers_help_dnn. intros b Hb. constructor. simpl. split. rewrite <- (Qmult_0_l a). apply Qmult_le_compat_r; assumption. rewrite Qmult_comm. rewrite <- (Qmult_1_l b) at 2. apply Qmult_le_compat_r. exact Ha1. exact Hb. apply powers_help_dnn. rewrite <- (Qmult_0_l a). apply Qmult_le_compat_r; assumption. Qed.
imports: CoRN.algebra.RSetoid CoRN.model.totalorder.QposMinMax CoRN.model.metric2.Qmetric CoRN.metric2.Limit Coq.QArith.Qabs Coq.Arith.Arith Coq.QArith.Qpower CoRN.reals.fast.LazyNat Coq.setoid_ring.Ring MathClasses.interfaces.abstract_algebra MathClasses.theory.streams MathClasses.theory.series MathClasses.interfaces.abstract_algebra MathClasses.theory.streams