proposition: Lemma log2_log2_up_spec : forall a, 0<a -> 2^log2 a <= a <= 2^log2_up a.
proof: Proof. intros a H. split. - now apply log2_spec. - rewrite <-le_succ_l, <-one_succ in H. le_elim H. + now apply log2_up_spec. + now rewrite <-H, log2_up_1, pow_0_r. Qed.
imports: NZAxioms NZMulOrder NZPow