proposition: Lemma mord_ext_l M N P : M >mul N <-> union P M >mul union P N.
proof: Proof. rewrite (union_comm P M), (union_comm P N). apply mord_ext_r. Qed.
imports: Coq(Transitive_Closure Compare_dec Relations Permutation Setoid Morphisms Basics Lia) CoLoR(RelExtras MultisetTheory ListPermutation MultisetCore ListExtras AccUtil LogicUtil)