proposition: Lemma Qpos_dlog2_spec (x : Q₊) : '(2 ^ Qdlog2 ('x)) ≤ ('x : Q) ∧ 'x < '(2 ^ (1 + Qdlog2 ('x))).
proof: Proof. unfold cast. simpl. split; apply Qdlog2_spec; now destruct x. 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