proposition: Lemma log2_add_le : forall a b, a~=1 -> b~=1 -> log2 (a+b) <= log2 a + log2 b.
proof: Proof. intros a b Ha Hb. destruct (lt_trichotomy a 1) as [Ha'|[Ha'|Ha']]; [|order|]. - rewrite one_succ, lt_succ_r in Ha'. rewrite (log2_nonpos a); trivial. nzsimpl. apply log2_le_mono. rewrite <- (add_0_l b) at 2. now apply add_le_mono. - destruct (lt_trichotomy b 1) as [Hb'|[Hb'|Hb']]; [|order|]. + rewrite one_succ, lt_succ_r in Hb'. rewrite (log2_nonpos b); trivial. nzsimpl. apply log2_le_mono. rewrite <- (add_0_r a) at 2. now apply add_le_mono. + clear Ha Hb. apply lt_succ_r. apply log2_lt_pow2; try order_pos. rewrite pow_succ_r by order_pos. rewrite two_succ, one_succ at 1. nzsimpl. apply add_lt_mono. * apply lt_le_trans with (2^(S (log2 a))). -- apply log2_spec; order'. -- apply pow_le_mono_r. ++ order'. ++ rewrite <- add_1_r. apply add_le_mono_l. rewrite one_succ; now apply le_succ_l, log2_pos. * apply lt_le_trans with (2^(S (log2 b))). -- apply log2_spec; order'. -- apply pow_le_mono_r. ++ order'. ++ rewrite <- add_1_l. apply add_le_mono_r. rewrite one_succ; now apply le_succ_l, log2_pos. Qed.
imports: NZAxioms NZMulOrder NZPow