exact
  ⟨ S',
    lt_of_lt_of_le (append_lt_sq_hash I L S (succ_le_iff_lt.mpr hintv) le_len_L (by simpa using pos_of_gt hintv)) hU,
    H',
    ext_append_lt I L S (succ_le_iff_lt.mpr hintv) (by simp),
    ext_append_last I L S (succ_le_iff_lt.mpr hintv) le_len_L ⟩
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))
le_len_L : ‖S{L}[intv] + fbit A (start + intv)‖ ≤ ‖L‖
H' : IsSegment L A start (intv + 1) S'
⊢ Segment U L A start (intv + 1) (S{L}[0]) (S{L}[intv] + fbit A (start + intv))
no goals