proposition: Lemma power_2_improve_bound_correct : forall (n:nat) (a:Q), a <= 0 -> -inject_Z (2^n) <= a -> -1 <= a*(1#2)^n <= 0.
proof: Proof. split. - apply (Qmult_le_r _ _ ((2#1)^n)). apply Q.Qpower_0_lt. reflexivity. apply (Qle_trans _ a). rewrite Zpower_Qpower in H0. exact H0. apply Nat2Z.is_nonneg. rewrite <- Qmult_assoc, <- Qmult_power. setoid_replace ((1 # 2) * 2)%Q with 1%Q by reflexivity. rewrite Qpower_1, Qmult_1_r. apply Qle_refl. - rewrite <- (Qmult_0_l ((1#2)^n)). apply Qmult_le_compat_r. exact H. apply Qpower_pos. discriminate. 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