proposition: Theorem permutation_transposition : forall a b l1 l2 l3, permutation (l1 ++ a :: l2 ++ b :: l3) (l1 ++ b :: l2 ++ a :: l3).
proof: Proof. intros a b l1 l2 l3. apply permutation_app_comp; auto. change (permutation ((a :: nil) ++ l2 ++ (b :: nil) ++ l3) ((b :: nil) ++ l2 ++ (a :: nil) ++ l3)) in |- *. repeat rewrite <- app_ass. apply permutation_app_comp; auto. apply permutation_trans with ((b :: nil) ++ (a :: nil) ++ l2); auto. apply permutation_app_swap; auto. repeat rewrite app_ass. apply permutation_app_comp; auto. apply permutation_app_swap; auto. Qed.
imports: List ListAux