proposition: Lemma mulOrd_oneElemDiff : forall l m a b, a >A b -> list2multiset (l ++ a::m) >MUL list2multiset (l ++ b::m).
proof: Proof. intros. constructor 1 with {{a}} {{b}} (list2multiset l + list2multiset m). auto with multisets. rewrite (list2multiset_app l (a::m)). simpl; solve_meq. rewrite (list2multiset_app l (b::m)). simpl; solve_meq. intros. exists a; auto with multisets. rewrite (member_singleton H0); trivial. Qed.
imports: Coq(Transitive_Closure Compare_dec Relations Permutation Setoid Morphisms Basics Lia) CoLoR(RelExtras MultisetTheory ListPermutation MultisetCore ListExtras AccUtil LogicUtil)