proposition: Lemma AQexp_inv_pos_bound_correct : '(cast (AQ₊) Q AQexp_inv_pos_bound) ≤ rational_exp ('a).
proof: Proof. change (cast Q CR (cast AQ Q ((1 ≪ (-2)) ^ Z.abs_N (Qfloor ('a)))) ≤ rational_exp ('a)). rewrite preserves_nat_pow. rewrite aq_shift_opp_2. rewrite rings.preserves_1, rings.mult_1_l. rewrite <-(int_pow_nat_pow (f:=cast N Z)). rewrite Z_of_N_abs, Z.abs_neq. apply (rational_exp_lower_bound (1#4)). now apply semirings.preserves_nonpos. apply CRpos_nonNeg. now CRsign.CR_solve_pos (1#1)%Qpos. change (Qfloor ('a) ≤ 0). apply (order_reflecting (cast Z Q)). transitivity ('a : Q). now apply Qfloor_le. now apply semirings.preserves_nonpos. 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