suffices log2' (n/2 + 1) ≤ n+1
  from log2'_div2 n ▸ Nat.succ_le_succ this
n : Nat
h_ind : log2' (n / 2 + 1) ≤ n / 2 + 1
⊢ log2' (n + 2) ≤ n + 2
n : Nat
h_ind : log2' (n / 2 + 1) ≤ n / 2 + 1
⊢ log2' (n / 2 + 1) ≤ n + 1