fact: Definition remove_min (L : list A) : (list A) * (option A) := match L with | nil => (L, None) | r :: L'' => (match foot_split L'' with (_, None) => nil | (L''', Some f) => sink (f :: L''', root_idx) end , Some r) end.
imports: Psatz List Arith.Div2 Even Relations RelationClasses PeanoNat Peano_dec Recdef Sorting Permutation Multiset