rewrite [as.size_pop, Nat.sub_sub, Nat.add_comm]
α : Type u
i k : Nat
IH : ∀ (as : Array α) (hk : k ≤ size as) (hi : i < size as - k), (shrink.loop k as)[i] = as[i]
as : Array α
hk : Nat.succ k ≤ size as
hi : i < size as - Nat.succ k
⊢ i < size (pop as) - k
α : Type u
i k : Nat
IH : ∀ (as : Array α) (hk : k ≤ size as) (hi : i < size as - k), (shrink.loop k as)[i] = as[i]
as : Array α
hk : Nat.succ k ≤ size as
hi : i < size as - Nat.succ k
⊢ i < size as - (k + 1)