proposition: Lemma CPermutation_split : forall l1 l2, CPermutation l1 l2 <-> exists n, l2 = skipn n l1 ++ firstn n l1.
proof: Proof. intros l1 l2; split. - intros [l1' l2']. exists (length l1'). rewrite skipn_app, skipn_all, Nat.sub_diag; simpl; f_equal. now rewrite firstn_app, firstn_all, Nat.sub_diag; simpl; rewrite app_nil_r. - now intros [n ->]; rewrite <- (firstn_skipn n) at 1. Qed.
imports: List Permutation Morphisms PeanoNat