let S' := append I L S (intv + 1) (S{L}[intv] + fbit A (start + intv))
case intro.intro.intro.intro
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
start intv : M
hintv : intv < ‖I‖
S : M
left✝ : S < U
H : IsSegment L A start intv S
hnₛ : ‖S{L}[0] + ‖I‖‖ ≤ ‖L‖
⊢ Segment U L A start (intv + 1) (S{L}[0]) (S{L}[intv] + fbit A (start + intv))
case intro.intro.intro.intro
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
start intv : M
hintv : intv < ‖I‖
S : M
left✝ : S < U
H : IsSegment L A start intv S
hnₛ : ‖S{L}[0] + ‖I‖‖ ≤ ‖L‖
S' : M := append I L S (intv + 1) (S{L}[intv] + fbit A (start + intv))
⊢ Segment U L A start (intv + 1) (S{L}[0]) (S{L}[intv] + fbit A (start + intv))