proposition: Lemma log2_unique : forall a b, 0<=b -> 2^b<=a<2^(S b) -> log2 a == b.
proof: Proof. intros a b Hb (LEb,LTb). assert (Ha : 0 < a). - apply lt_le_trans with (2^b); trivial. apply pow_pos_nonneg; order'. - assert (Hc := log2_nonneg a). destruct (log2_spec a Ha) as (LEc,LTc). assert (log2 a <= b). + apply lt_succ_r, (pow_lt_mono_r_iff 2); try order'. now apply le_le_succ_r. + assert (b <= log2 a). * apply lt_succ_r, (pow_lt_mono_r_iff 2); try order'. now apply le_le_succ_r. * order. Qed.
imports: NZAxioms NZMulOrder NZPow