case div2 n h_ind =>
  rw [recBase2_div2, h_ind]
  conv =>
    rhs; unfold log2; rw [if_pos (Nat.le_add_left 2 n), Nat.add_div_right n (Nat.zero_lt_succ 1)]
n : Nat
h_ind : recBase2 0 0 (fun x x_1 => x_1 + 1) (n / 2 + 1) = log2 (n / 2 + 1)
⊢ recBase2 0 0 (fun x x_1 => x_1 + 1) (n + 2) = log2 (n + 2)
no goals