proposition: Lemma log2_mul_above : forall a b, 0<=a -> 0<=b -> log2 (a*b) <= log2 a + log2 b + 1.
proof: Proof. intros a b Ha Hb. le_elim Ha. - le_elim Hb. + apply lt_succ_r. rewrite add_1_r, <- add_succ_r, <- add_succ_l. apply log2_lt_pow2; try order_pos. rewrite pow_add_r by order_pos. apply mul_lt_mono_nonneg; try order; now apply log2_spec. + rewrite <- Hb. nzsimpl. rewrite log2_nonpos; order_pos. - rewrite <- Ha. nzsimpl. rewrite log2_nonpos; order_pos. Qed.
imports: NZAxioms NZMulOrder NZPow