proposition: Lemma log2_mul_pow2 : forall a b, 0<a -> 0<=b -> log2 (a*2^b) == b + log2 a.
proof: Proof. intros a b Ha Hb. apply log2_unique; try order_pos. split. - rewrite pow_add_r, mul_comm; try order_pos. apply mul_le_mono_nonneg_r. + order_pos. + now apply log2_spec. - rewrite <-add_succ_r, pow_add_r, mul_comm; try order_pos. apply mul_lt_mono_pos_l. + order_pos. + now apply log2_spec. Qed.
imports: NZAxioms NZMulOrder NZPow