proposition: Lemma mord_inclusion : forall M N, MultisetGt R' M N -> MultisetGt R M N.
proof: Proof. intros M N M_N. induction M_N. constructor 1. inversion H. constructor 1 with X a Y; trivial. intros b b_Y. apply R'sub. apply H2; trivial. constructor 2 with y; trivial. Qed.
imports: Coq(Transitive_Closure Compare_dec Relations Permutation Setoid Morphisms Basics Lia) CoLoR(RelExtras MultisetTheory ListPermutation MultisetCore ListExtras AccUtil LogicUtil)