case div2 n h_ind =>
  rw [log2'_div2]
  show 2^(log2' (n/2+1) + 1) ≤ n+2
  calc
    2^(log2' (n/2+1) + 1)
      = 2^(log2' (n/2+1)) * 2 := Nat.pow_succ 2 _
    _ ≤ (n/2+1) * 2 := Nat.mul_le_mul_right 2 (h_ind $ Nat.zero_lt_succ _)
    _ = n/2*2 + 2 := Nat.add_mul _ 1 2
    _ ≤ n+2 := Nat.add_le_add_right (Nat.div_mul_le_self n 2) 2
n : Nat
h_ind : n / 2 + 1 > 0 → 2 ^ log2' (n / 2 + 1) ≤ n / 2 + 1
h : n + 2 > 0
⊢ 2 ^ log2' (n + 2) ≤ n + 2
no goals