Theorem: Subarray.size_shrinkOne' (Algdata/Data/Array/Subarray.lean)

State before:
α : Type u
x : Subarray α
h : x.start < x.stop
⊢ x.stop - 1 - x.start = x.stop - x.start - 1
Tactic:
simp only [Nat.sub_sub, Nat.add_comm 1 x.start]
State after:
no goals