suffices log2' (n/2 + 1) < n+1
  from log2'_div2 n ▸ Nat.succ_lt_succ this
n : Nat
h_ind : n / 2 + 1 > 0 → log2' (n / 2 + 1) < n / 2 + 1
hpos : n + 2 > 0
⊢ log2' (n + 2) < n + 2
n : Nat
h_ind : n / 2 + 1 > 0 → log2' (n / 2 + 1) < n / 2 + 1
hpos : n + 2 > 0
⊢ log2' (n / 2 + 1) < n + 1