proposition: Lemma mOrd_dec : forall M N, {M >MUL N} + {~M >MUL N}.
proof: Proof. intros. apply mOrd_dec_aux. intros. change (~m >A n) with (m <=A n). apply gtA_dec. Qed.
imports: Coq(Transitive_Closure Compare_dec Relations Permutation Setoid Morphisms Basics Lia) CoLoR(RelExtras MultisetTheory ListPermutation MultisetCore ListExtras AccUtil LogicUtil)