proposition: Lemma list2multiset_diff_length : forall l m n, list2multiset l =mul= list2multiset m - list2multiset n -> length l >= length m - length n.
proof: Proof. induction l. simpl; intros. rewrite (diff_empty m n); auto with multisets arith. intros; simpl. assert (length l >= length m - (length (a :: n))). apply IHl. simpl in H. rewrite (meq_remove H). simpl; solve_meq. simpl in H0; lia. Qed.
imports: Coq(List Setoid Morphisms) CoLoR(RelExtras MultisetCore ListPermutation NatUtil ListExtras LogicUtil)