proposition: Lemma log2_mul_below : forall a b, 0<a -> 0<b -> log2 a + log2 b <= log2 (a*b).
proof: Proof. intros a b Ha Hb. apply log2_le_pow2; try order_pos. rewrite pow_add_r by order_pos. apply mul_le_mono_nonneg; try apply log2_spec; order_pos. Qed.
imports: NZAxioms NZMulOrder NZPow