proposition: Lemma irrefl_to_mult_irrefl : transitive r -> forall ss, (forall s, In s ss -> r s s -> False) -> mult ss ss -> False.
proof: Proof. unfold mult; intros Htrans ss Hsub H. apply (irrefl_to_MultisetGT_irrefl Htrans (list2multiset ss)). intros m m_in_ss Hm; apply (Hsub m); trivial. elim (member_multiset_list ss m_in_ss). apply In_eqA_compat. gen H; unfold MultisetLT; simpl; trivial. Qed.
imports: Coq(List Permutation Arith Morphisms Basics) CoLoR(MultisetOrder RelExtras MultisetCore MultisetList MultisetTheory AccUtil RelUtil LogicUtil) CoLoR(AccUtil ListUtil)