proposition: Lemma transp_trans_to_mult_trans : forall us, (forall u, In u us -> forall t s, transp r u t -> transp r t s -> transp r u s) -> forall ts ss, mult us ts -> mult ts ss -> mult us ss.
proof: Proof. intros us Hsub ts ss; unfold mult, MultisetLT, transp; intros H1 H2. assert (Hsub' : forall p, p in (list2multiset us) -> forall x y, r x p -> r y x -> r y p). intros p p_in_us x y H H'. elim (member_multiset_list us p_in_us); intros p' p'_in_us p'eq. apply r_eqA_compat with y p'; auto with multisets. auto with sets. auto with sets. gen (Hsub p' p'_in_us x y); unfold transp; simpl; intro Hsub'; apply Hsub'; trivial. apply r_eqA_compat with x p; auto with multisets. auto with sets. apply (sub_transp_trans_2_mOrd_trans Hsub') with (list2multiset ts); trivial. Qed.
imports: Coq(List Permutation Arith Morphisms Basics) CoLoR(MultisetOrder RelExtras MultisetCore MultisetList MultisetTheory AccUtil RelUtil LogicUtil) CoLoR(AccUtil ListUtil)