rcases show l ≤ iter from lt_succ_iff_le.mp hl with (rfl | hl)
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
L✝ A✝ U I L A : M
hU : (I # L) ^ 2 ≤ U
hIL : ‖‖I‖ ^ 2‖ ≤ ‖L‖
Ipos : 0 < I
iter n' : M
hiter : iter < ‖I‖
T : M
left✝ : T < U
HT : IsSeries U I L A iter T
Tₛ : T{L}[0] = 0
HS : Segment U L A (‖I‖ * iter) ‖I‖ (T{L}[iter]) n'
Hn : T{L}[iter] ≤ ‖I‖ * iter
T' : M := append I L T (iter + 1) n'
hn'L : ‖n'‖ ≤ ‖L‖
hTlast : T'{L}[iter + 1] = n'
hTofLt : ∀ l ≤ iter, T'{L}[l] = T{L}[l]
l : M
hl : l < iter + 1
⊢ Segment U L A (‖I‖ * l) ‖I‖ (T'{L}[l]) (T'{L}[l + 1])
case inl
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
L✝ A✝ U I L A : M
hU : (I # L) ^ 2 ≤ U
hIL : ‖‖I‖ ^ 2‖ ≤ ‖L‖
Ipos : 0 < I
n' T : M
left✝ : T < U
Tₛ : T{L}[0] = 0
hn'L : ‖n'‖ ≤ ‖L‖
l : M
hiter : l < ‖I‖
HT : IsSeries U I L A l T
HS : Segment U L A (‖I‖ * l) ‖I‖ (T{L}[l]) n'
Hn : T{L}[l] ≤ ‖I‖ * l
T' : M := append I L T (l + 1) n'
hTlast : T'{L}[l + 1] = n'
hTofLt : ∀ l_1 ≤ l, T'{L}[l_1] = T{L}[l_1]
hl : l < l + 1
⊢ Segment U L A (‖I‖ * l) ‖I‖ (T'{L}[l]) (T'{L}[l + 1])

case inr
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
L✝ A✝ U I L A : M
hU : (I # L) ^ 2 ≤ U
hIL : ‖‖I‖ ^ 2‖ ≤ ‖L‖
Ipos : 0 < I
iter n' : M
hiter : iter < ‖I‖
T : M
left✝ : T < U
HT : IsSeries U I L A iter T
Tₛ : T{L}[0] = 0
HS : Segment U L A (‖I‖ * iter) ‖I‖ (T{L}[iter]) n'
Hn : T{L}[iter] ≤ ‖I‖ * iter
T' : M := append I L T (iter + 1) n'
hn'L : ‖n'‖ ≤ ‖L‖
hTlast : T'{L}[iter + 1] = n'
hTofLt : ∀ l ≤ iter, T'{L}[l] = T{L}[l]
l : M
hl✝ : l < iter + 1
hl : l < iter
⊢ Segment U L A (‖I‖ * l) ‖I‖ (T'{L}[l]) (T'{L}[l + 1])