proposition: Lemma meq_ins_ins a a' M M' : M + {{a}} =mul= M' + {{a'}} -> M =mul= M' + {{a'}} - {{a}}.
proof: Proof. intros. try_solve_meq. assert ((x/M)%msets + (x/{{a}})%msets = (x/M')%msets + (x/{{a'}})%msets)%nat. rewrite <- !union_mult. apply meq_multeq; trivial. lia. Qed.
imports: Coq(List Setoid Morphisms) CoLoR(RelExtras MultisetCore ListPermutation NatUtil ListExtras LogicUtil)