proposition: Lemma remove_min_root: forall L, match remove_min L with | (L', None) => L = L' /\ L' = nil | (L', Some a) => nth_error L root_idx = Some a end.
proof: Proof. unfold remove_min. destruct L; auto. Qed.
imports: Psatz List Arith.Div2 Even Relations RelationClasses PeanoNat Peano_dec Recdef Sorting Permutation Multiset