proposition: Lemma Qpow_bounded_Zshiftl (x n : Z) : 'Z.shiftl x n ≤ cast Z Q x * 2 ^ n < 'Z.shiftl x n + 1.
proof: Proof. destruct (total (≤) 0 n) as [En | En]. rewrite Z.shiftl_mul_pow2 by trivial. rewrite inject_Z_mult. rewrite Qpower.Zpower_Qpower by trivial. split; try reflexivity. apply semirings.pos_plus_lt_compat_r. now apply (semirings.lt_0_1 (R:=Q)). rewrite Z.shiftl_div_pow2 by trivial. assert (('x * 2 ^ n : Q) = 'x / 'Zpower 2 (-n)). rewrite Qpower.Zpower_Qpower. rewrite <-Qpower.Qpower_opp, Z.opp_involutive. reflexivity. now apply rings.flip_nonpos_negate in En. split. transitivity ('x / 'Zpower 2 (-n) : Q). now apply Qdiv_bounded_Zdiv. apply orders.eq_le. now symmetry. apply orders.le_lt_trans with ('x / 'Zpower 2 (-n) : Q). now apply orders.eq_le. now apply Qdiv_bounded_Zdiv. Qed.
imports: CoRN.algebra.RSetoid CoRN.metric2.Metric CoRN.metric2.UniformContinuity Coq.Program.Program Coq.QArith.QArith Coq.ZArith.ZArith Bignums.BigZ.BigZ CoRN.model.totalorder.QposMinMax CoRN.metric2.MetricMorphisms CoRN.model.metric2.Qmetric CoRN.util.Qdlog CoRN.reals.faster.ARArith MathClasses.theory.int_pow MathClasses.theory.nat_pow MathClasses.interfaces.rationals MathClasses.implementations.stdlib_rationals MathClasses.interfaces.integers MathClasses.implementations.stdlib_binary_integers MathClasses.implementations.fast_integers MathClasses.implementations.dyadics