proposition: Lemma log2_up_le_pow2 : forall a b, 0<a -> (a<=2^b <-> log2_up a <= b).
proof: Proof. intros a b Ha. split; intros H. - destruct (lt_ge_cases b 0) as [Hb|Hb]. + rewrite pow_neg_r in H; order. + rewrite <- (log2_up_pow2 b); trivial. now apply log2_up_le_mono. - transitivity (2^(log2_up a)). + now apply log2_log2_up_spec. + apply pow_le_mono_r; order'. Qed.
imports: NZAxioms NZMulOrder NZPow