proposition: Lemma log2_up_spec : forall a, 1<a -> 2^(P (log2_up a)) < a <= 2^(log2_up a).
proof: Proof. intros a Ha. rewrite log2_up_eqn; trivial. rewrite pred_succ. rewrite <- (lt_succ_pred 1 a Ha) at 2 3. rewrite lt_succ_r, le_succ_l. apply log2_spec. apply succ_lt_mono. now rewrite (lt_succ_pred 1 a Ha), <- one_succ. Qed.
imports: NZAxioms NZMulOrder NZPow