proposition: Lemma log2_up_succ_le : forall a, log2_up (S a) <= S (log2_up a).
proof: Proof. intros a. destruct (lt_trichotomy 1 a) as [LT|[EQ|LT]]. - rewrite 2 log2_up_eqn; trivial. + rewrite pred_succ, <- succ_le_mono. rewrite <-(lt_succ_pred 1 a LT) at 1. apply log2_succ_le. + apply lt_succ_r; order. - rewrite <- EQ, <- two_succ, log2_up_1, log2_up_2. now nzsimpl'. - rewrite 2 log2_up_eqn0. + order_pos. + order'. + now rewrite le_succ_l. Qed.
imports: NZAxioms NZMulOrder NZPow