proposition: Lemma Qdlog2_unique (x : Q) (y : Z) : 0 < x → 2 ^ y ≤ x ∧ x < 2 ^ (1 + y) → y = Qdlog2 x.
proof: Proof. intros. apply (antisymmetry (≤)). apply nat_int.le_iff_lt_plus_1. rewrite commutativity. apply int_pow_exp_lt_back with (2%mc : Q); [ apply semirings.lt_1_2 |]. apply orders.le_lt_trans with x; [ intuition |]. now apply Qdlog2_spec. apply nat_int.le_iff_lt_plus_1. rewrite commutativity. apply int_pow_exp_lt_back with (2%mc : Q); [ apply semirings.lt_1_2 |]. apply orders.le_lt_trans with x; [|intuition]. now apply Qdlog2_spec. 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