proposition: Lemma log2_up_mul_pow2 : forall a b, 0<a -> 0<=b -> log2_up (a*2^b) == b + log2_up a.
proof: Proof. intros a b Ha Hb. rewrite <- le_succ_l, <- one_succ in Ha; le_elim Ha. - apply log2_up_unique. + apply add_nonneg_pos; trivial. now apply log2_up_pos. + split. * assert (EQ := lt_succ_pred 0 _ (log2_up_pos _ Ha)). rewrite <- EQ. nzsimpl. rewrite pow_add_r, mul_comm; trivial. -- apply mul_lt_mono_pos_r. ++ order_pos. ++ now apply log2_up_spec. -- rewrite <- lt_succ_r, EQ. now apply log2_up_pos. * rewrite pow_add_r, mul_comm; trivial. -- apply mul_le_mono_nonneg_l. ++ order_pos. ++ now apply log2_up_spec. -- apply log2_up_nonneg. - now rewrite <- Ha, mul_1_l, log2_up_1, add_0_r, log2_up_pow2. Qed.
imports: NZAxioms NZMulOrder NZPow