proposition: Lemma powers_help_nbz : forall x, 0 <= x <= 1 -> NearBy 0 (Qpos2QposInf (1#1)) (powers_help a x).
proof: Proof. cofix powers_help_nbz. intros b [Hb0 Hb1]. destruct Ha as [Ha0 Ha1]. constructor. simpl. unfold Qball. unfold QAbsSmall. setoid_replace (b-0)%Q with b. 2: unfold Qminus; apply Qplus_0_r. split;simpl. apply Qle_trans with 0;[discriminate|assumption]. assumption. simpl. apply powers_help_nbz. split. rewrite <- (Qmult_0_l a). apply Qmult_le_compat_r; assumption. apply (Qle_trans _ (1*a)). apply Qmult_le_compat_r; assumption. rewrite Qmult_1_l. exact Ha1. 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