proposition: Lemma add_log2_up_lt : forall a b, 0<a -> 0<b -> log2_up a + log2_up b < 2 * log2_up (a+b).
proof: Proof. intros a b Ha Hb. nzsimpl'. assert (H : log2_up a <= log2_up (a+b)). - apply log2_up_le_mono. rewrite <- (add_0_r a) at 1. apply add_le_mono; order. - assert (H' : log2_up b <= log2_up (a+b)). + apply log2_up_le_mono. rewrite <- (add_0_l b) at 1. apply add_le_mono; order. + le_elim H. * apply lt_le_trans with (log2_up (a+b) + log2_up 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_up_same in H; try order_pos. symmetry in H'. apply log2_up_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