proposition: Lemma mord_ext_r: forall M N P, M >mul N <-> M + P >mul N + P.
proof: Proof. intros; induction P as [ | P] using mset_ind. rewrite (union_empty M), (union_empty N); split; auto. rewrite (union_assoc M P {{a}}), (union_assoc N P {{a}}). split; intro ord. rewrite_lr (mord_ext1 (M + P) (N + P) a). rewrite_lr IHP; trivial. rewrite_rl IHP. rewrite_rl (mord_ext1 (M + P) (N + P) a); trivial. Qed.
imports: Coq(Transitive_Closure Compare_dec Relations Permutation Setoid Morphisms Basics Lia) CoLoR(RelExtras MultisetTheory ListPermutation MultisetCore ListExtras AccUtil LogicUtil)