proposition: Lemma log2_up_succ_double : forall a, 0<a -> log2_up (2*a+1) == 2 + log2 a.
proof: Proof. intros a Ha. rewrite log2_up_eqn. - rewrite add_1_r, pred_succ, log2_double; now nzsimpl'. - apply le_lt_trans with (0+1). + now nzsimpl'. + apply add_lt_mono_r. order_pos. Qed.
imports: NZAxioms NZMulOrder NZPow