case div2 n h_ind =>
  suffices log2' (n/2 + 1) ≤ n+1
    from log2'_div2 n ▸ Nat.succ_le_succ this
  calc
    log2' (n/2 + 1)
      ≤ n/2 + 1 := h_ind
    _ ≤ n + 1 := Nat.succ_le_succ (Nat.div_le_self n 2)
n : Nat
h_ind : log2' (n / 2 + 1) ≤ n / 2 + 1
⊢ log2' (n + 2) ≤ n + 2
no goals