case succ i IH =>
  intro h
  have IH : S{L}[i] ≤ S{L}[0] + i := IH (le_trans (by simp) h)
  calc
    S{L}[i + 1] = S{L}[i] + fbit A (start + i) := H i (succ_le_iff_lt.mp h)
    _           ≤ S{L}[i] + 1                  := by simp
    _           ≤ S{L}[0] + (i + 1)            := by simp [←add_assoc, IH]
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
L✝ A✝ L A start intv S : M
H : IsSegment L A start intv S
i : M
IH : i ≤ intv → S{L}[i] ≤ S{L}[0] + i
⊢ i + 1 ≤ intv → S{L}[i + 1] ≤ S{L}[0] + (i + 1)
no goals