proposition: Lemma multiset_closure_aux3 : forall l lc cns, permut (consn l) (lc ++ cns) -> exists ll, exists ll', LLP.permut l (ll ++ ll') /\ permut (consn ll) lc /\ permut (consn ll') cns.
proof: Proof. assert (H : forall consnl lccns, permut consnl lccns -> forall l lc cns , consnl = consn l -> lccns = lc ++ cns -> exists ll, exists ll', LLP.permut l (ll ++ ll') /\ permut (consn ll) lc /\ permut (consn ll') cns). intros consnl lccns P; induction P as [ | a1 a1' consnl k1 k2 H P]. intros [ | [a1 l1] l]. intros [ | c lc]. intros [ | c' cns] H1 H2. exists (@nil (A * list A)); exists (@nil (A * list A)); simpl; repeat split; auto. discriminate. intros cns _ H2; discriminate. intros lc cns H1; discriminate. intros [ | [b1 l1] l] lc cns H1 H2. discriminate. injection H1; clear H1; intros; subst. generalize (split_list _ _ _ _ H2); clear H2; intros [[k [H3 H4]] | [k [H3 H4]]]; subst. generalize (IHP l lc (k ++ k2) (eq_refl _)); rewrite ass_app. intro IH; generalize (IH (eq_refl _)); clear IH. intros [ll [ll' [Q1 [Q2 Q3]]]]. exists ll; exists ((b1,l1) :: ll'); simpl; repeat split; trivial. rewrite <- LLP.permut_cons_inside; [assumption | apply eq_refl]. rewrite <- permut_cons_inside; assumption. revert H4; case k; [idtac | intros a k']; intro H4. simpl in H4; subst. generalize (IHP l k1 k2 (eq_refl _) (eq_refl _)). intros [ll [ll' [Q1 [Q2 Q3]]]]. exists ll; exists ((b1,l1) :: ll'); repeat split. rewrite <- LLP.permut_cons_inside; [assumption | apply eq_refl]. rewrite <- app_nil_end; assumption. simpl; rewrite <- permut_cons; assumption. injection H4; clear H4; intros; subst a k2. assert (IH := IHP l (k1 ++ k') cns (eq_refl _)). rewrite ass_app in IH. generalize (IH (eq_refl _)); clear IH; intros [ll [ll' [Q1 [Q2 Q3]]]]. exists ((b1, l1) :: ll); exists ll'; repeat split. simpl; rewrite <- LLP.permut_cons; [assumption | apply eq_refl]. simpl; rewrite <- permut_cons_inside; assumption. assumption. intros l lc cns P; apply (H (consn l) (lc ++ cns) P _ _ _ (eq_refl _) (eq_refl _)). Qed.
imports: Coq(Relations List Multiset Arith Morphisms FunInd) CoLoR(closure more_list list_permut ordered_set)