proposition: Lemma meq_remove_elem_right a M L R : M + {{a}} =mul= L + R -> a in R -> M =mul= L + (remove a R).
proof: Proof. intros. rewrite (union_comm L (remove a R)), <- (remove_union L H0), (union_comm R L), <- H. solve_meq. Qed.
imports: Coq(List Setoid Morphisms) CoLoR(RelExtras MultisetCore ListPermutation NatUtil ListExtras LogicUtil)