proposition: Lemma direct_subset_red : forall M N, M >MUL N -> M >mul N.
proof: Proof. destruct 1. generalize dependent Y. generalize dependent Z. generalize M N. generalize dependent X. induction X as [ | X] using mset_ind. intros; absurd (empty <>mul empty); auto with multisets. intros; case (empty_dec X). intro X_empty. assert (X + {{a}} =mul= {{a}}); [ rewrite X_empty; eauto with multisets | idtac]. constructor; constructor 1 with Z a Y. solve_meq_ext. trivial. intros y yY; destruct (H2 y); trivial. assert (x in {{a}}); [rewrite <- H3; trivial | idtac]. assert (x =A= a); [apply member_singleton; trivial | idtac]. rewrite <- H7; trivial. intro X_nempty. destruct (partition2 H2) as [Yg [Yl Ydec [Yg_ord Yl_ord]]]. constructor 2 with (Z + Yl + {{a}}). apply IHX with (Z + {{a}}) Yl; try solve [auto with multisets | solve_meq_ext]. constructor; constructor 1 with (Z + Yl) a Yg. solve_meq_ext. solve_meq_ext. trivial. Qed.
imports: Coq(Transitive_Closure Compare_dec Relations Permutation Setoid Morphisms Basics Lia) CoLoR(RelExtras MultisetTheory ListPermutation MultisetCore ListExtras AccUtil LogicUtil)