. exact as.size.sub_le_self n
case refine_1
α : Type u
as : Array α
n : Nat
h : n ≤ size as
⊢ size as - n ≤ size as

case refine_2
α : Type u
as : Array α
n : Nat
h : n ≤ size as
⊢ size as - (size as - n) = n
case refine_2
α : Type u
as : Array α
n : Nat
h : n ≤ size as
⊢ size as - (size as - n) = n