simp only [Nat.succ_sub_succ_eq_sub]
case succ
α : Type u
k : Nat
IH : ∀ (as : Array α), k ≤ size as → size (shrink.loop k as) = size as - k
as : Array α
h : Nat.succ k ≤ size (pop as) + 1
this : size as = size (pop as) + 1
⊢ size (pop as) - k = size (pop as) + 1 - Nat.succ k
no goals