proposition: Lemma list_sim_remove : forall M M' a b, P a b -> a in M -> list_sim P (multiset2list (remove a M)) M' -> exists M'', list2multiset M'' =mul= insert b (list2multiset M') /\ list_sim P (multiset2list M) M''.
proof: Proof. intros M M' a b Pab aM MM'_sim. destruct (list_sim_insert (remove a M) Pab MM'_sim) as [C [CbM' Csim]]. destruct (@list_sim_permutation A P eqA eqA_dec eqA_Equivalence P_eqA_comp (multiset2list (insert a (remove a M))) C (multiset2list M)) as [C' [C'sim C'perm]]; trivial. apply meq_permutation. rewrite (double_convertion M), (double_convertion (insert a (remove a M))). apply multeq_meq; intro x. mset_unfold; unfold member in aM. destruct (eqA_dec x a); autorewrite with multisets. rewrite !singleton_mult_in; trivial. rewrite <- (mult_eqA_compat M e) in aM. lia. rewrite !singleton_mult_notin; trivial. lia. exists C'; split; trivial. rewrite <- (permutation_meq C'perm); trivial. Qed.
imports: Coq(Transitive_Closure Compare_dec Relations Permutation Setoid Morphisms Basics Lia) CoLoR(RelExtras MultisetTheory ListPermutation MultisetCore ListExtras AccUtil LogicUtil)