rw [IH, size_as_popMax]
case succ
α : Type u
lt : α → α → Bool
x : Subarray α
n : Nat
y : Array α
x✝ : Subarray α
n✝ : Nat
y✝ : Array α
h : loop.OpSpec lt (popMax lt x✝) n✝ y✝
IH : Array.size y✝ = Array.size (popMax lt x✝).as
⊢ Array.size y✝ = Array.size x✝.as
no goals