no goals
α : Type u_1
le : α → α → Bool
a : α
s' s : Heap α
eq : deleteMin le s = some (a, s')
⊢ size s' < size s
cases s with cases eq | node a c => simp_arith [size_combine, size]
no goals
case node.refl
α : Type u_1
le : α → α → Bool
a : α
c sibling✝ : Heap α
⊢ size (combine le c) < size (node a c sibling✝)
simp_arith [size_combine, size]