proposition: Lemma list_sim_insert : forall M M' a b, P a b -> list_sim P (multiset2list M) M' -> exists M'', list2multiset M'' =mul= insert b (list2multiset M') /\ list_sim P (multiset2list (insert a M)) M''.
proof: Proof. intros M M' a b Pab MM'. destruct (multiset2list_insert a M) as [a' [p [a'a [Mperm Mp]]]]. destruct (list_sim_permutation eqA_Equivalence P_eqA_comp MM' Mperm) as [M'' [M''sim M'M'']]. exists (insert_nth M'' p b); split. rewrite (list2multiset_insert_nth b M'' p), (permutation_meq M'M''); auto with multisets. assert (length M'' >= p). rewrite <- (list_sim_length M''sim). set (h := drop_nth_length (multiset2list (insert a M)) p). set (h' := nth_some (multiset2list (insert a M)) p Mp). lia. apply (@list_sim_insert_nth A A P p (multiset2list (insert a M)) (insert_nth M'' p b) a' b); trivial. apply nth_insert_nth; trivial. replace a' with a; trivial. rewrite <- eqA_eq; trivial. rewrite drop_nth_insert_nth; trivial. Qed.
imports: Coq(Transitive_Closure Compare_dec Relations Permutation Setoid Morphisms Basics Lia) CoLoR(RelExtras MultisetTheory ListPermutation MultisetCore ListExtras AccUtil LogicUtil)