proposition: Lemma Qpower_le_1 : forall (a : Q) (p : positive), 0 <= a <= 1 -> 0 <= a ^ p <= 1.
proof: Proof. split. - apply Qpower_pos, H. - revert p. apply Pos.peano_ind. apply H. intros p Hp. unfold Qpower. rewrite <- Pos.add_1_l, Qpower_plus_positive. apply (Qle_trans _ (1*Qpower_positive a p)). apply Qmult_le_compat_r. apply H. apply (Qpower_pos a p), H. rewrite Qmult_1_l. apply Hp. Qed.
imports: CoRN.metric2.Metric CoRN.metric2.UniformContinuity CoRN.model.totalorder.QMinMax CoRN.reals.fast.CRAlternatingSum CoRN.reals.fast.CRAlternatingSum_alg CoRN.reals.fast.CRstreams CoRN.reals.fast.CRArith CoRN.reals.fast.CRIR CoRN.reals.iso_CReals Coq.QArith.Qpower CoRN.algebra.COrdFields2 CoRN.model.ordfields.Qordfield CoRN.transc.PowerSeries CoRN.reals.fast.CRpower CoRN.transc.Exponential CoRN.transc.RealPowers CoRN.reals.fast.Compress Coq.NArith.Ndigits CoRN.reals.fast.ModulusDerivative CoRN.reals.fast.ContinuousCorrect CoRN.reals.fast.CRsign CoRN.reals.Q_in_CReals Coq.QArith.Qabs Coq.QArith.Qround CoRN.tactics.CornTac MathClasses.theory.int_pow MathClasses.interfaces.abstract_algebra