proposition: Lemma mOrd_dec_aux : forall M N, (forall m n, m in M -> n in N -> {m >A n} + {~m >A n}) -> {M >MUL N} + {~M >MUL N}.
proof: Proof. intros. destruct (mult_split M N). destruct (@many_one_dec (Multiset*Multiset*Multiset) Multiset (fun LRS N => Ord (fst (fst LRS)) (snd (fst LRS))) x N). intros. destruct x0 as [[L R] S]. apply Ord_dec; simpl; intros. destruct (proj1 (a L R S) H). apply X. rewrite H2; auto with multisets. rewrite H3; auto with multisets. destruct s as [[[L R] S] [LRSx LRSord]]. simpl in LRSord; inversion LRSord. destruct (proj1 (a L R S) LRSx). left; constructor 1 with L R S; trivial. right; intro MN; inversion MN. destruct (proj2 (a X0 Y Z) H0 H1) as [L [R [S [XL [YR [ZS LRSx]]]]]]. absurd (Ord L R). apply (n (L, R, S)); trivial. split; trivial. rewrite <- XL; trivial. intros. destruct (H2 r). rewrite YR; trivial. exists x0; trivial. rewrite <- XL; trivial. Qed.
imports: Coq(Transitive_Closure Compare_dec Relations Permutation Setoid Morphisms Basics Lia) CoLoR(RelExtras MultisetTheory ListPermutation MultisetCore ListExtras AccUtil LogicUtil)