BinaryHeap.size_pos_of_max

theorem BinaryHeap.size_pos_of_max : ∀ {α : Type u_1} {x : α} {lt : α → α → Bool} {self : BinaryHeap α lt}, self.max = some x → 0 < self.size

This theorem states that for any type `α`, any element `x` of type `α`, a binary heap `self` of type `α` and a binary relation `lt` of type `α → α → Bool`, if the maximum element of the binary heap `self` is `x` (i.e., `BinaryHeap.max self` equals `some x`), then the size of the binary heap `self` must be greater than zero. That is, the heap is non-empty.

More concisely: If `self` is a binary heap of type `α` with maximum element `x` of type `α`, then `#self > 0`. (Here, `#self` represents the size of the binary heap.)