proposition: Lemma Qdlog2_mult_pow2 (x : Q) (n : Z) : 0 < x → Qdlog2 x + n = Qdlog2 (mult x (2 ^ n)).
proof: Proof. intros E. apply Qdlog2_unique. apply pos_mult_compat; [easy | solve_propholds]. split. rewrite int_pow_exp_plus by solve_propholds. apply (order_preserving (.* 2 ^ n)). now apply Qdlog2_spec. rewrite associativity. rewrite int_pow_exp_plus by solve_propholds. apply (strictly_order_preserving (.* 2 ^ n)). 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