proposition: Lemma CPermutation_vs_cons_inv : forall l l0 a, CPermutation l (a :: l0) -> exists l' l'', l0 = l'' ++ l' /\ l = l' ++ a :: l''.
proof: Proof. intros; rewrite <- (app_nil_r l0); now apply CPermutation_vs_elt_inv. Qed.
imports: List Permutation Morphisms PeanoNat