proposition: Lemma Qdlog2_nonneg (x : Q) : 1 ≤ x → 0 ≤ Qdlog2 x.
proof: Proof. intros E. unfold Qdlog2. case (decide_rel _); intros. now mc_setoid_replace x with (1:Q) by now apply (antisymmetry (≤)). apply Z.log2_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