proposition: Lemma irrefl_to_MultisetGT_irrefl : transitive r -> forall M, (forall m, m in M -> r m m -> False) -> MultisetGT r M M -> False.
proof: Proof. intros Htrans M Hsub HM. inversion HM. assert (H' : X =mul= Y). apply meq_union_meq with Z. rewrite (union_comm X Z), (union_comm Y Z), <- H1, <- H0. auto with multisets. assert (H'' : forall (x : A), x in X -> ex (fun (x' : A) => x' in X /\ r x' x)). intros x x_in_X; assert (x_in_Y : x in Y). rewrite <- H'; trivial. elim (H2 x x_in_Y); intros x' Hx'1 Hx'2. exists x'; split; trivial. elim (self_dom Htrans X H H''); intros x Hx. elim Hx; clear Hx; intros Hx1 Hx2. apply (Hsub x); trivial. rewrite H0, (union_comm Z X); auto with multisets. Qed.
imports: Coq(List Permutation Arith Morphisms Basics) CoLoR(MultisetOrder RelExtras MultisetCore MultisetList MultisetTheory AccUtil RelUtil LogicUtil) CoLoR(AccUtil ListUtil)