proposition: Lemma log2_up_pow2 : forall a, 0<=a -> log2_up (2^a) == a.
proof: Proof. intros a Ha. le_elim Ha. - apply log2_up_unique; trivial. split; try order. apply pow_lt_mono_r; try order'. rewrite <- (lt_succ_pred 0 a Ha) at 2. now apply lt_succ_r. - now rewrite <- Ha, pow_0_r, log2_up_eqn0. Qed.
imports: NZAxioms NZMulOrder NZPow