proposition: Lemma log2_up_mul_above : forall a b, 0<=a -> 0<=b -> log2_up (a*b) <= log2_up a + log2_up b.
proof: Proof. intros a b Ha Hb. assert (Ha':=log2_up_nonneg a). assert (Hb':=log2_up_nonneg b). le_elim Ha. - le_elim Hb. + apply log2_up_le_pow2; try order_pos. rewrite pow_add_r; trivial. apply mul_le_mono_nonneg; try apply log2_log2_up_spec; order'. + rewrite <- Hb. nzsimpl. rewrite log2_up_nonpos; order_pos. - rewrite <- Ha. nzsimpl. rewrite log2_up_nonpos; order_pos. Qed.
imports: NZAxioms NZMulOrder NZPow