proposition: Lemma log2_up_lt_pow2 : forall a b, 0<a -> (2^b<a <-> b < log2_up a).
proof: Proof. intros a b Ha. split; intros H. - destruct (lt_ge_cases b 0) as [Hb|Hb]. + generalize (log2_up_nonneg a); order. + apply (pow_lt_mono_r_iff 2). * order'. * apply log2_up_nonneg. * apply lt_le_trans with a; trivial. apply (log2_up_spec a). apply le_lt_trans with (2^b); trivial. rewrite one_succ, le_succ_l. apply pow_pos_nonneg; order'. - destruct (lt_ge_cases b 0) as [Hb|Hb]. + now rewrite pow_neg_r. + rewrite <- (log2_up_pow2 b) in H; trivial. now apply log2_up_lt_cancel. Qed.
imports: NZAxioms NZMulOrder NZPow