proposition: Lemma mult2element : forall ss ts, mult ss ts -> forall s, In s ss -> ex (fun t => In t ts /\ (t =A= s \/ r t s)).
proof: Proof. unfold mult; intros ss ts Hmult s s_in_ss; inversion Hmult. cut (s in (list2multiset ss)). intro s_in_mult_ss. cut (s in Z \/ s in Y). intro case_s; elim case_s; clear case_s; intro case_s. exists s; split. elim (member_multiset_list ts) with s; trivial. apply In_eqA_compat. rewrite H0. apply member_member_union; hyp. left; auto with multisets. auto with sets. elim (H2 s case_s); intros t' t'_in_X Ht'. exists t'; split. elim (member_multiset_list ts) with t'; trivial. apply In_eqA_compat. rewrite H0, (union_comm Z X). apply member_member_union; hyp. right; hyp. apply member_union. rewrite <- H1; apply member_list_multiset; hyp. apply member_list_multiset; hyp. Qed.
imports: Coq(List Permutation Arith Morphisms Basics) CoLoR(MultisetOrder RelExtras MultisetCore MultisetList MultisetTheory AccUtil RelUtil LogicUtil) CoLoR(AccUtil ListUtil)