rewrite [Subarray.size, ← Nat.add_sub_assoc (Nat.sub_pos_of_lt hs), Nat.add_sub_cancel' x.h₁]
case hc
α : Type u
lt : α → α → Bool
x : Subarray α
hs : x.start < x.stop
⊢ x.start + (Subarray.size x - 1) = x.stop - 1
case hc
α : Type u
lt : α → α → Bool
x : Subarray α
hs : x.start < x.stop
⊢ x.stop - Nat.succ 0 = x.stop - 1