proposition: Lemma power_2_improve_bound_correct : forall (n:nat), -2 ^ n ≤ a -> -1 ≤ a*(1 ≪ (-1))^n ≤ 0.
proof: Proof. intros. assert ('a <= 0)%Q as aneg. { apply (order_preserving (cast AQ Q)) in Pa. rewrite rings.preserves_0 in Pa. exact Pa. } pose proof (CRexp.power_2_improve_bound_correct n aneg) as H6. assert ('(-1) <= '(a * (1 ≪ (-1)) ^ n) <= '0 -> -1 ≤ a * (1 ≪ (-1)) ^ n ≤ 0). { intros. split; apply (order_reflecting (cast AQ Q)); apply H7. } apply H7. clear H7. rewrite rings.preserves_mult. rewrite rings.preserves_negate. rewrite rings.preserves_1. rewrite rings.preserves_0. rewrite preserves_nat_pow. rewrite <-(int_pow_nat_pow (f:=Z_of_nat)). rewrite (aq_shift_correct 1 (-1)). rewrite rings.preserves_1. rewrite Qmult_1_l. apply H6. clear H6. apply (order_preserving (cast AQ Q)) in H5. refine (Qle_trans _ _ _ _ H5). rewrite rings.preserves_negate. rewrite preserves_nat_pow. rewrite <-(int_pow_nat_pow (f:=Z_of_nat)). rewrite Qpower.Zpower_Qpower. rewrite rings.preserves_2. apply Qle_refl. apply Nat2Z.is_nonneg. Qed.
imports: CoRN.algebra.RSetoid CoRN.metric2.Metric CoRN.metric2.UniformContinuity Coq.Program.Program MathClasses.misc.workaround_tactics CoRN.model.totalorder.QposMinMax CoRN.model.totalorder.QMinMax Coq.QArith.Qround Coq.QArith.Qabs CoRN.util.Qdlog CoRN.stdlib_omissions.Q CoRN.reals.fast.CRexp CoRN.reals.fast.CRstreams CoRN.reals.fast.CRAlternatingSum CoRN.reals.fast.Compress CoRN.reals.fast.CRpower CoRN.metric2.MetricMorphisms CoRN.reals.faster.ARAlternatingSum MathClasses.interfaces.abstract_algebra MathClasses.orders.minmax MathClasses.theory.nat_pow MathClasses.theory.int_pow CoRN.reals.faster.ARArith