proposition: Lemma dom_dec : forall M n, (forall m, m in M -> {m >A n} + {~m >A n}) -> {m: A | m in M /\ m >A n} + {forall m, m in M -> ~m >A n}.
proof: Proof. intro M. apply mset_ind_type with (P := fun M => forall n, (forall m, m in M -> {m >A n} + {~m >A n}) -> {m: A | m in M /\ m >A n} + {forall m, m in M -> ~m >A n}). right; intros. exfalso; apply not_empty with empty m; auto with multisets. intros. destruct (X n) as [[m [mM0 mn]] | nm]. intros; apply X0; auto with multisets. left; exists m; auto with multisets. destruct (X0 a); auto with multisets. left; exists a; auto with multisets. right; intros. destruct (member_union H). apply nm; trivial. rewrite (member_singleton H0); trivial. Qed.
imports: Coq(Transitive_Closure Compare_dec Relations Permutation Setoid Morphisms Basics Lia) CoLoR(RelExtras MultisetTheory ListPermutation MultisetCore ListExtras AccUtil LogicUtil)