proposition: Lemma Qdlog2_0 (x : Q) : 0 < x → Qdlog2 x = 0 → x < 2.
proof: Proof. intros E1 E2. pose proof (Qdlog2_spec x E1) as E3. now rewrite E2 in E3. 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