proposition: Lemma list2multiset_union_length : forall l m n, list2multiset l =mul= list2multiset m + list2multiset n -> length l = (length m + length n)%nat.
proof: Proof. induction l; simpl; intros. destruct m. destruct n; trivial. exfalso; apply not_empty with (list2multiset (a::n)) a. simpl; unfold insert; auto with multisets. rewrite H; solve_meq. exfalso; apply not_empty with (list2multiset (a::m) + list2multiset n) a. simpl; unfold insert; auto with multisets. rewrite H; solve_meq. destruct (@member_union a (list2multiset m) (list2multiset n)). rewrite <- H; auto with multisets. unfold insert; apply member_union_l; auto with multisets. rewrite (IHl (removeElem eqA eqA_dec a m) n). rewrite (removeElem_length_in). destruct m; simpl; trivial. exfalso; apply not_empty with (list2multiset nil) a; trivial. simpl; auto with multisets. destruct (member_multiset_list m H0). exists x; split; trivial. rewrite <- (list2multiset_remove_in a m). rewrite <- (remove_union (list2multiset n) H0). apply insert_meq with a. assert (a in (list2multiset m + list2multiset n)). apply member_union_l; trivial. rewrite (meq_insert_remove H1); trivial. rewrite (IHl m (removeElem eqA eqA_dec a n)). rewrite (removeElem_length_in). destruct n; simpl; trivial. exfalso; apply not_empty with (list2multiset nil) a; trivial. simpl; auto with multisets. destruct (member_multiset_list n H0). exists x; split; trivial. rewrite <- (list2multiset_remove_in a n). rewrite (union_comm (list2multiset m) (remove a (list2multiset n))). rewrite <- (remove_union (list2multiset m) H0). apply insert_meq with a. assert (a in (list2multiset m + list2multiset n)). apply member_union_r; trivial. rewrite (union_comm (list2multiset n) (list2multiset m)). rewrite (meq_insert_remove H1); trivial. Qed.
imports: Coq(List Setoid Morphisms) CoLoR(RelExtras MultisetCore ListPermutation NatUtil ListExtras LogicUtil)