proposition: Lemma log2_lt_pow2 : forall a b, 0<a -> (a<2^b <-> log2 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. + apply (pow_lt_mono_r_iff 2); try order_pos. apply le_lt_trans with a; trivial. now destruct (log2_spec a Ha). - destruct (lt_ge_cases b 0) as [Hb|Hb]. + generalize (log2_nonneg a); order. + apply log2_lt_cancel; try order. now rewrite log2_pow2. Qed.
imports: NZAxioms NZMulOrder NZPow