proposition: Lemma Ord_dec : forall M N, (forall m n, m in M -> n in N -> {m >A n} + {~m >A n}) -> {Ord M N} + {~Ord M N}.
proof: Proof. intros M N; gen M; clear M. apply mset_ind_type with (P := fun N => forall M, (forall m n, m in M -> n in N -> {m >A n} + {~m >A n}) -> {Ord M N} + {~Ord M N}); intros. destruct (empty_dec M). right; intro MN; inversion MN; try_solve. left; split; trivial. intros; exfalso. apply not_empty with empty r; auto with multisets. clear N. destruct (X M0). intros; apply X0; trivial. apply member_member_union; trivial. destruct (@dom_dec M0 a) as [[m [mM0 mma]] | nm]. intros; apply X0; trivial. auto with multisets. inversion o. left; split; trivial. intros; destruct (member_union H1). apply H0; trivial. exists m; trivial. rewrite (member_singleton H2); trivial. right; intro MN; inversion MN. destruct (H0 a). auto with multisets. apply (nm x); trivial. right; intro MN; inversion MN. apply n; split; trivial; intros. apply H0; auto with multisets. Qed.
imports: Coq(Transitive_Closure Compare_dec Relations Permutation Setoid Morphisms Basics Lia) CoLoR(RelExtras MultisetTheory ListPermutation MultisetCore ListExtras AccUtil LogicUtil)