proposition: Lemma partition : forall M, exists Mp, exists2 Mq, M =mul= Mp + Mq & (forall p, p in Mp -> P p) /\ (forall q, q in Mq -> Q q).
proof: Proof. induction M using mset_ind. exists empty; exists empty. solve_meq. split; intros. absurd (p in empty); eauto with multisets. absurd (q in empty); eauto with multisets. decompose record IHM. case (PQ_dec a); intro wa. exists (x + {{a}}); exists x0. rewrite (union_perm x {{a}} x0); auto with multisets. split; intros. case (member_union H1); intro wp. apply H; trivial. assert (pa : a =A= p); [ auto with multisets sets | apply (P_comp pa); trivial]. apply H2; trivial. exists x; exists (x0 + {{a}}). rewrite (union_assoc x x0 {{a}}); auto with multisets. split; intros. apply H; trivial. case (member_union H1); intro wp. apply H2; trivial. assert (pa : a =A= q); [ auto with multisets sets | apply (Q_comp pa); trivial]. Qed.
imports: Coq(List Setoid Morphisms) CoLoR(RelExtras MultisetCore ListPermutation NatUtil ListExtras LogicUtil)