proposition: Lemma Qdlog4_spec (x : Q) : 0 < x → 4 ^ Qdlog4 x ≤ x ∧ x < 4 ^ (1 + Qdlog4 x).
proof: Proof. intros E1. unfold Qdlog4. change (4%mc:Q) with ((2%mc:Q) ^ (2:Z))%mc. rewrite <-2!int_pow_exp_mult. split. etransitivity. 2: now apply Qdlog2_spec. apply int_pow_exp_le; [easy|]. now apply Z.mul_div_le. eapply orders.lt_le_trans. now apply Qdlog2_spec. apply int_pow_exp_le; [apply semirings.le_1_2 |]. apply nat_int.le_iff_lt_plus_1. rewrite commutativity. apply (strictly_order_preserving (+1)). change (1 + (Qdlog2 x / 2)%Z) with (1 + Z.div (Qdlog2 x) 2)%Z. rewrite (Z.add_1_l (Z.div (Qdlog2 x) 2)). now apply Z.mul_succ_div_gt. Qed.
imports: Coq.ZArith.ZArith Coq.QArith.QArith Coq.QArith.Qround CoRN.stdlib_omissions.Q MathClasses.interfaces.abstract_algebra MathClasses.interfaces.additional_operations MathClasses.interfaces.orders MathClasses.theory.int_pow MathClasses.orders.rationals MathClasses.implementations.stdlib_rationals MathClasses.implementations.positive_semiring_elements