no goals
α : Type u_1
le : α → α → Bool
a : α
s' s : Heap α
h : NoSibling s
eq : deleteMin le s = some (a, s')
⊢ size s = size s' + 1
cases h with cases eq | node a c => rw [size_combine, size, size]
no goals
case node.refl
α : Type u_1
le : α → α → Bool
a : α
c : Heap α
⊢ size (node a c nil) = size (combine le c) + 1
rw [size_combine, size, size]