simp only [Subarray.size, Nat.sub_sub_self x.h₁]
case refine_1
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
i j : Nat
hi : x.start ≤ i
hij : i < j
hj : j < x.stop
⊢ x.stop - Subarray.size x ≤ i
case refine_1
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
i j : Nat
hi : x.start ≤ i
hij : i < j
hj : j < x.stop
⊢ x.start ≤ i