case succ i IH =>
  intro hi
  have IH : T₁{L}[i] = T₂{L}[i] := IH (le_trans (by simp) hi)
  have h₁ : Segment U L A (‖I‖ * i) ‖I‖ (T₁{L}[i]) (T₁{L}[i + 1]) := HT₁ i (lt_iff_succ_le.mpr hi)
  have h₂ : Segment U L A (‖I‖ * i) ‖I‖ (T₁{L}[i]) (T₂{L}[i + 1]) := by simpa [IH] using HT₂ i (lt_iff_succ_le.mpr hi)
  exact h₁.uniq h₂
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 iter T₁ : M
left✝¹ : T₁ < U
HT₁ : IsSeries U I L A iter T₁
Hₛ₁ : T₁{L}[0] = 0
T₂ : M
left✝ : T₂ < U
HT₂ : IsSeries U I L A iter T₂
Hₛ₂ : T₂{L}[0] = 0
i : M
IH : i ≤ iter → T₁{L}[i] = T₂{L}[i]
⊢ i + 1 ≤ iter → T₁{L}[i + 1] = T₂{L}[i + 1]
no goals