proposition: Lemma add_log2_lt : forall a b, 0<a -> 0<b -> log2 a + log2 b < 2 * log2 (a+b).
proof: Proof. intros a b Ha Hb. nzsimpl'. assert (H : log2 a <= log2 (a+b)). - apply log2_le_mono. rewrite <- (add_0_r a) at 1. apply add_le_mono; order. - assert (H' : log2 b <= log2 (a+b)). + apply log2_le_mono. rewrite <- (add_0_l b) at 1. apply add_le_mono; order. + le_elim H. * apply lt_le_trans with (log2 (a+b) + log2 b). -- now apply add_lt_mono_r. -- now apply add_le_mono_l. * rewrite <- H at 1. apply add_lt_mono_l. le_elim H'; trivial. symmetry in H. apply log2_same in H; try order_pos. symmetry in H'. apply log2_same in H'; try order_pos. revert H H'. nzsimpl'. rewrite <- add_lt_mono_l, <- add_lt_mono_r; order. Qed.
imports: NZAxioms NZMulOrder NZPow