proposition: Lemma le_log2_up_succ_log2 : forall a, log2_up a <= S (log2 a).
proof: Proof. intros a. unfold log2_up. case compare_spec; intros H; try order_pos. rewrite <- succ_le_mono. apply log2_le_mono. rewrite <- (lt_succ_pred 1 a H) at 2. apply le_succ_diag_r. Qed.
imports: NZAxioms NZMulOrder NZPow