proposition: Lemma log2_up_add_le : forall a b, a~=1 -> b~=1 -> log2_up (a+b) <= log2_up a + log2_up b.
proof: Proof. intros a b Ha Hb. destruct (lt_trichotomy a 1) as [Ha'|[Ha'|Ha']]; [|order|]. - rewrite (log2_up_eqn0 a) by order. nzsimpl. apply log2_up_le_mono. rewrite one_succ, lt_succ_r in Ha'. rewrite <- (add_0_l b) at 2. now apply add_le_mono. - destruct (lt_trichotomy b 1) as [Hb'|[Hb'|Hb']]; [|order|]. + rewrite (log2_up_eqn0 b) by order. nzsimpl. apply log2_up_le_mono. rewrite one_succ, lt_succ_r in Hb'. rewrite <- (add_0_r a) at 2. now apply add_le_mono. + clear Ha Hb. transitivity (log2_up (a*b)). * now apply log2_up_le_mono, add_le_mul. * apply log2_up_mul_above; order'. Qed.
imports: NZAxioms NZMulOrder NZPow