proposition: Lemma red_eq_direct : forall M N, M >mul N <-> M >MUL N.
proof: Proof. intros; split. induction 1. inversion H. constructor 1 with {{a}} Y X; solve [ solve_meq_ext | eauto with multisets ]. apply mOrd_trans with y; trivial. apply direct_subset_red. Qed.
imports: Coq(Transitive_Closure Compare_dec Relations Permutation Setoid Morphisms Basics Lia) CoLoR(RelExtras MultisetTheory ListPermutation MultisetCore ListExtras AccUtil LogicUtil)