proposition: Lemma partition2 : forall Y X a, (forall y, y in Y -> exists2 x : A, x in (X + {{a}}) & x >A y) -> exists Ya, (exists2 Yx : Multiset, Y =mul= Ya + Yx & (forall y, y in Ya -> a >A y) /\ (forall y, y in Yx -> exists2 x, x in X & x >A y)).
proof: Proof. induction Y as [ | Y] using mset_ind. intros; exists empty; exists empty. solve_meq. split; intros. unfold member in H0; rewrite (empty_mult y) in H0; inversion H0. unfold member in H0; rewrite (empty_mult y) in H0; inversion H0. intros X a'; intros. cut (forall y : A, y in Y -> exists2 x : A, x in (X + {{a'}}) & x >A y). intro H'. elim (IHY X a' H'). intros Ya HYa. elim HYa; clear HYa; intros Yx HY HYx. elim HYx; clear HYx; intros HYa HYx. cut (a in (Y + {{a}})). intro Ha; elim (H a Ha); intros x' Hx' Hx'2. elim (member_union Hx'); intro case_x'. exists Ya; exists (Yx + {{a}}). rewrite HY. auto with multisets. split. hyp. intros y Hy. elim (member_union Hy); intro case_y. apply HYx; trivial. exists x'; trivial. generalize (member_singleton case_y) Hx'2; intro y_is_a. apply gtA_eqA_compat; auto with multisets. rewrite y_is_a; auto with multisets. exists (Ya + {{a}}); exists Yx. rewrite HY. solve_meq. split. intros y Hy. elim (member_union Hy); intro case_y. apply HYa; trivial. gen Hx'2; apply gtA_eqA_compat. apply (member_singleton case_x'). rewrite (member_singleton case_y); auto with multisets. hyp. rewrite (union_comm Y {{a}}). apply member_member_union. apply singleton_member. intros y HY; apply H. apply member_member_union; trivial. Qed.
imports: Coq(Transitive_Closure Compare_dec Relations Permutation Setoid Morphisms Basics Lia) CoLoR(RelExtras MultisetTheory ListPermutation MultisetCore ListExtras AccUtil LogicUtil)