proposition: Lemma log2_up_succ_pow2 : forall a, 0<=a -> log2_up (S (2^a)) == S a.
proof: Proof. intros a Ha. rewrite log2_up_eqn, pred_succ, log2_pow2; try easy. rewrite one_succ, <- succ_lt_mono. apply pow_pos_nonneg; order'. Qed.
imports: NZAxioms NZMulOrder NZPow