proposition: Lemma multiset2list_insert a M : exists a' p, a =A= a' /\ permutation eqA_dec (multiset2list M) (drop_nth (multiset2list (insert a M)) p) /\ nth_error (multiset2list (insert a M)) p = Some a'.
proof: Proof. unfold multiset2list; intros. destruct (mult_to_list M). destruct (mult_to_list (insert a M)). destruct (@member_multiset_list x0 a) as [a' a'x0 a'a]. rewrite <- m0; apply member_insert. destruct (list_In_nth x0 a' a'x0) as [p x0p]. exists a'; exists p; split; trivial; split; trivial. apply permutation_drop with a a'; trivial. exact eqA_Equivalence. apply meq_permutation. simpl. rewrite <- m; trivial. Qed.
imports: Coq(List Setoid Morphisms) CoLoR(RelExtras MultisetCore ListPermutation NatUtil ListExtras LogicUtil)