proposition: Lemma log2_up_mul_below : forall a b, 0<a -> 0<b -> log2_up a + log2_up b <= S (log2_up (a*b)).
proof: Proof. intros a b Ha Hb. rewrite <-le_succ_l, <-one_succ in Ha. le_elim Ha. - rewrite <-le_succ_l, <-one_succ in Hb. le_elim Hb. + assert (Ha' : 0 < log2_up a) by (apply log2_up_pos; trivial). assert (Hb' : 0 < log2_up b) by (apply log2_up_pos; trivial). rewrite <- (lt_succ_pred 0 (log2_up a)); trivial. rewrite <- (lt_succ_pred 0 (log2_up b)); trivial. nzsimpl. rewrite <- succ_le_mono, le_succ_l. apply (pow_lt_mono_r_iff 2). * order'. * apply log2_up_nonneg. * rewrite pow_add_r; try (apply lt_succ_r; rewrite (lt_succ_pred 0); trivial). apply lt_le_trans with (a*b). -- apply mul_lt_mono_nonneg; try order_pos; try now apply log2_up_spec. -- apply log2_up_spec. setoid_replace 1 with (1*1) by now nzsimpl. apply mul_lt_mono_nonneg; order'. + rewrite <- Hb, log2_up_1; nzsimpl. apply le_succ_diag_r. - rewrite <- Ha, log2_up_1; nzsimpl. apply le_succ_diag_r. Qed.
imports: NZAxioms NZMulOrder NZPow