proposition: Lemma CPermutation_vs_elt_inv : forall l l1 l2 a, CPermutation l (l1 ++ a :: l2) -> exists l' l'', l2 ++ l1 = l'' ++ l' /\ l = l' ++ a :: l''.
proof: Proof. intros l l1 l2 a HC. inversion HC as [l1' l2' Heq' Heq]; clear HC; subst. enough (exists l3, (l2' ++ l3 = l1 /\ l1' = l3 ++ a :: l2) \/ (l2' = l1 ++ a :: l3 /\ l3 ++ l1' = l2)) as [l3 [[<- ->]|[-> <-]]]. - exists l3, (l2 ++ l2'); rewrite app_comm_cons; intuition. - exists (l1' ++ l1), l3; intuition. - revert l1' l2' l2 Heq; induction l1; simpl; intros l1' l2' l2 Heq. + destruct l2'; inversion Heq; subst. * exists nil; intuition. * exists l2'; intuition. + destruct l2'; inversion Heq; subst. * exists (a0 :: l1); intuition. * apply IHl1 in H1 as [l3 [[<- ->]|[-> <-]]]; exists l3; intuition. Qed.
imports: List Permutation Morphisms PeanoNat