proposition: Lemma log2_up_le_mono : forall a b, a<=b -> log2_up a <= log2_up b.
proof: Proof. intros a b H. destruct (le_gt_cases a 1) as [Ha|Ha]. - rewrite log2_up_eqn0; trivial. apply log2_up_nonneg. - rewrite 2 log2_up_eqn; try order. rewrite <- succ_le_mono. apply log2_le_mono, succ_le_mono. rewrite 2 lt_succ_pred with 1; order. Qed.
imports: NZAxioms NZMulOrder NZPow