case div2 m h_ind =>
  intro h
  let k := n-2
  have : n = k+2 := Eq.symm $ Nat.sub_add_cancel $ calc
    2 ≤ m+2 := Nat.le_add_left 2 m
    _ ≤ n := h
  rw [this]; unfold log2'; simp [recBase2_div2]
  conv => change (m/2+1).log2' + 1 ≤ (k/2+1).log2' + 1
  suffices m/2+1 ≤ k/2+1
    from Nat.succ_le_succ (h_ind this)
  suffices m ≤ k
    from Nat.succ_le_succ (div_le_div this)
  show m ≤ k;
    exact Nat.le_of_add_le_add_right (‹n=k+2› ▸ h)
m : Nat
h_ind : ∀ {n : Nat}, m / 2 + 1 ≤ n → log2' (m / 2 + 1) ≤ log2' n
n : Nat
⊢ m + 2 ≤ n → log2' (m + 2) ≤ log2' n
no goals