proposition: Theorem CPermutation_trans : forall l l' l'', CPermutation l l' -> CPermutation l' l'' -> CPermutation l l''.
proof: Proof. intros l l' l'' HC1 HC2. inversion HC1 as [l1 l2]; inversion HC2 as [l3 l4 Heq Heq']; subst. clear - Heq; revert l1 l2 l4 Heq; clear; induction l3; simpl; intros. - now subst; rewrite app_nil_r. - destruct l2 as [| b]. + simpl in Heq; subst. now rewrite app_nil_r, app_comm_cons. + inversion Heq as [[Heqb Heq']]; subst. replace (l1 ++ b :: l2) with ((l1 ++ b :: nil) ++ l2) by now rewrite <- app_assoc, <- app_comm_cons. replace (l4 ++ b :: l3) with ((l4 ++ b :: nil) ++ l3) by now rewrite <- app_assoc, <- app_comm_cons. apply IHl3. now rewrite 2 app_assoc, Heq'. Qed.
imports: List Permutation Morphisms PeanoNat