proposition: Lemma self_dom : transitive r -> forall X, X <>mul empty -> (forall x, x in X -> ex (fun x' => x' in X /\ r x' x)) -> ex (fun x => x in X /\ r x x).
proof: Proof. intro Htrans. apply (nonempty_mset_ind (fun (X : Multiset) => (forall (x : A), x in X -> ex (fun (x' : A) => x' in X /\ r x' x)) -> ex (fun (x : A) => x in X /\ r x x))). intros M N HM Heq H1. assert (H : exists x : A, x in M /\ r x x). apply HM. intros x x_in_M; assert (H : x in N). rewrite <- Heq; auto with multisets. elim (H1 x H); intros x' Hx'; elim Hx'; clear Hx'; intros Hx'1 Hx'2; exists x'; split; trivial. rewrite Heq; auto with multisets. elim H; clear H; intros x H; elim H; clear H; intros H H'; exists x; split; trivial. rewrite <- Heq; auto with multisets. intros a Ha; exists a; split; auto with multisets. elim (Ha a (singleton_member a)); intros x' Hx'; elim Hx'; clear Hx'; intros Hx'1 Hx'2. apply (r_eqA_compat x' a a a). apply member_singleton. hyp. auto with sets. hyp. intros a M HM H. assert (H' : a in (M + {{a}})); auto with multisets. elim (H a H'); intros x' Hx'; elim Hx'; clear Hx'; intros Hx'1 Hx'2. elim (member_union Hx'1); intro case_x'. assert (H'' : exists x : A, x in M /\ r x x). apply HM. intros x x_in_M; assert (H'' : x in (M + {{a}})); auto with multisets. elim (H x H''); intros x0 Hx0; elim Hx0; clear Hx0; intros Hx01 Hx02. elim (member_union Hx01); intro case_x0. exists x0; split; trivial. exists x'; split; trivial. apply Htrans with a; trivial. apply (r_eqA_compat x0 a x x); auto with sets multisets. elim H''; intros x Hx; elim Hx; clear Hx; intros Hx1 Hx2. exists x; split; trivial. auto with multisets. exists a; split; auto with multisets. apply (r_eqA_compat x' a a a); auto with sets multisets. Qed.
imports: Coq(List Permutation Arith Morphisms Basics) CoLoR(MultisetOrder RelExtras MultisetCore MultisetList MultisetTheory AccUtil RelUtil LogicUtil) CoLoR(AccUtil ListUtil)