induction k generalizing as with
| zero => rfl
| succ k IH =>
  dsimp [shrink.loop]
  have : as.size = as.pop.size + 1 := by
    rw [as.size_pop, Nat.sub_add_cancel (trans (r:=LE.le (α:=Nat)) (s:=LT.lt (α:=Nat)) k.zero_le h)]
  rewrite [this] at h ⊢
  rewrite [IH as.pop (Nat.le_of_succ_le_succ h)]
  simp only [Nat.succ_sub_succ_eq_sub]
α : Type u
as : Array α
k : Nat
h : k ≤ size as
⊢ size (shrink.loop k as) = size as - k
no goals