proposition: Lemma remove_min_permutation: forall L, match remove_min L with | (L', None) => L = L' /\ L' = nil | (L', Some m) => Permutation L (m :: L') end.
proof: Proof. intros. unfold remove_min. destruct L. auto. constructor. clear a. generalize (foot_split_spec _ L). case_eq (foot_split L). intros. destruct o; intros; subst. transitivity (a :: l). rewrite Permutation_app_comm. trivial. apply sink_permutation. destruct H0. subst. constructor. Qed.
imports: Psatz List Arith.Div2 Even Relations RelationClasses PeanoNat Peano_dec Recdef Sorting Permutation Multiset