proposition: Lemma log2_up_unique : forall a b, 0<b -> 2^(P b)<a<=2^b -> log2_up a == b.
proof: Proof. intros a b Hb (LEb,LTb). assert (Ha : 1 < a). - apply le_lt_trans with (2^(P b)); trivial. rewrite one_succ. apply le_succ_l. apply pow_pos_nonneg. + order'. + apply lt_succ_r. now rewrite (lt_succ_pred 0 b Hb). - assert (Hc := log2_up_nonneg a). destruct (log2_up_spec a Ha) as (LTc,LEc). assert (b <= log2_up a). + apply lt_succ_r. rewrite <- (lt_succ_pred 0 b Hb). rewrite <- succ_lt_mono. apply (pow_lt_mono_r_iff 2); try order'. + assert (Hc' : 0 < log2_up a) by order. assert (log2_up a <= b). * apply lt_succ_r. rewrite <- (lt_succ_pred 0 _ Hc'). rewrite <- succ_lt_mono. apply (pow_lt_mono_r_iff 2); try order'. * order. Qed.
imports: NZAxioms NZMulOrder NZPow