proposition: Lemma Qdlog2_preserving (x y : Q) : 0 < x → x ≤ y → Qdlog2 x ≤ Qdlog2 y.
proof: Proof. intros E1 E2. 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; [now apply Qdlog2_spec | ]. apply orders.le_lt_trans with y; [assumption |]. apply Qdlog2_spec. now apply orders.lt_le_trans with 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