proposition: Lemma le_log2_log2_up : forall a, log2 a <= log2_up a.
proof: Proof. intros a. unfold log2_up. case compare_spec; intros H. - rewrite <- H, log2_1. order. - rewrite <- (lt_succ_pred 1 a H) at 1. apply log2_succ_le. - rewrite log2_nonpos. + order. + now rewrite <-lt_succ_r, <-one_succ. Qed.
imports: NZAxioms NZMulOrder NZPow