proposition: Lemma list2multiset_insert_nth a l p : list2multiset (insert_nth l p a) =mul= insert a (list2multiset l).
proof: Proof. intros. change (insert a (list2multiset l)) with (list2multiset (a :: l)). apply permutation_meq. apply insert_nth_permut. Qed.
imports: Coq(List Setoid Morphisms) CoLoR(RelExtras MultisetCore ListPermutation NatUtil ListExtras LogicUtil)