proposition: Lemma log2_le_pow2 : forall a b, 0<a -> (2^b<=a <-> b <= log2 a).
proof: Proof. intros a b Ha. split; intros H. - destruct (lt_ge_cases b 0) as [Hb|Hb]. + generalize (log2_nonneg a); order. + rewrite <- (log2_pow2 b); trivial. now apply log2_le_mono. - transitivity (2^(log2 a)). + apply pow_le_mono_r; order'. + now destruct (log2_spec a Ha). Qed.
imports: NZAxioms NZMulOrder NZPow