proposition: Lemma log2_pred_pow2 : forall a, 0<a -> log2 (P (2^a)) == P a.
proof: Proof. intros a Ha. assert (Ha' : S (P a) == a) by (now rewrite lt_succ_pred with 0). apply log2_unique. - apply lt_succ_r; order. - rewrite <-le_succ_l, <-lt_succ_r, Ha'. rewrite lt_succ_pred with 0. + split; try easy. apply pow_lt_mono_r_iff; try order'. rewrite succ_lt_mono, Ha'. apply lt_succ_diag_r. + apply pow_pos_nonneg; order'. Qed.
imports: NZAxioms NZMulOrder NZPow