proposition: Lemma remove_min_dec: forall L, match remove_min L with | (L', None) => L = L' /\ L' = nil | (L', Some a) => 1 + length L' = length L end.
proof: Proof. intros. generalize (remove_min_permutation L). case (remove_min L). destruct o; auto. intro. apply Permutation_length in H. simpl in H. lia. Qed.
imports: Psatz List Arith.Div2 Even Relations RelationClasses PeanoNat Peano_dec Recdef Sorting Permutation Multiset