proposition: Lemma diff_empty : forall l m, list2multiset l - list2multiset m =mul= empty -> (length l - length m = 0)%nat.
proof: Proof. induction l. auto. intros. simpl in H. destruct (insert_diff H). assert (length m > 0). destruct (member_multiset_list m H0). destruct m. inversion H2. simpl; auto with arith. assert ((length l - pred (length m) = 0)%nat). set (w := IHl (removeElem eqA eqA_dec a m)). rewrite removeElem_length_in in w. apply w. rewrite <- H1. rewrite (list2multiset_remove_in a m); auto with multisets. destruct (member_multiset_list m H0). exists x; split; trivial. destruct (length m); simpl in *; lia. Qed.
imports: Coq(List Setoid Morphisms) CoLoR(RelExtras MultisetCore ListPermutation NatUtil ListExtras LogicUtil)