proposition: Lemma remove_union a L R : a in L -> remove a (L + R) =mul= (remove a L) + R.
proof: Proof. intros. apply multeq_meq; intros. unfold remove. repeat (rewrite diff_mult || rewrite union_mult). destruct (eqA_dec x a). rewrite singleton_mult_in; trivial. rewrite (mult_eqA_compat L e). unfold member in H; lia. rewrite singleton_mult_notin; trivial. lia. Qed.
imports: Coq(List Setoid Morphisms) CoLoR(RelExtras MultisetCore ListPermutation NatUtil ListExtras LogicUtil)