have IH : S{L}[i] ≤ S{L}[0] + i := IH (le_trans (by simp) h)
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
h : i + 1 ≤ intv
⊢ S{L}[i + 1] ≤ S{L}[0] + (i + 1)
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
h : i + 1 ≤ intv
IH : S{L}[i] ≤ S{L}[0] + i
⊢ S{L}[i + 1] ≤ S{L}[0] + (i + 1)