proposition: Lemma Qdlog_spec (n : Z) (x : Q) : 2 ≤ n → 1 ≤ x → 'n ^ Qdlog n x ≤ x ∧ x < 'n ^ (1 + Qdlog n x).
proof: Proof. intros. apply Qdlog_spec_bounded; trivial. rewrite inj_Zabs_nat, Z.abs_eq; [reflexivity |]. now apply Qdlog2_nonneg. 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