theorem Batteries.BinomialHeap.Imp.Heap.findMin_val {α : Type u_1} {s : Heap α} {le : α → α → Bool} {k : Heap α → Heap α} {res : FindMin α} : (findMin le k s res).val = headD le res.val s

theorem Batteries.BinomialHeap.Imp.Heap.deleteMin_fst {α : Type u_1} {s : Heap α} {le : α → α → Bool} : Option.map (fun (x : α × Heap α) => x.fst) (deleteMin le s) = head? le s

@[simp]

theorem Batteries.BinomialHeap.Imp.HeapNode.WF.realSize_eq {α : Type u_1} {le : α → α → Bool} {a : α} {n : Nat} {s : HeapNode α} : WF le a s n → s.realSize + 1 = 2 ^ n

@[simp]

theorem Batteries.BinomialHeap.Imp.Heap.WF.size_eq {α : Type u_1} {le : α → α → Bool} {n : Nat} {s : Heap α} : WF le n s → s.size = s.realSize