proposition: Theorem perm_transposition : forall a b (l1 l2 l3 : list A), Permutation (l1 ++ a :: l2 ++ b :: l3) (l1 ++ b :: l2 ++ a :: l3).
proof: Proof. intros a b l1 l2 l3. apply Permutation_app; auto. change (Permutation ((a :: nil) ++ l2 ++ (b :: nil) ++ l3) ((b :: nil) ++ l2 ++ (a :: nil) ++ l3)) in |- *. repeat rewrite <- app_ass. apply Permutation_app; auto. apply perm_trans with ((b :: nil) ++ (a :: nil) ++ l2); auto. apply Permutation_app_comm; auto. repeat rewrite app_ass. apply Permutation_app; auto. apply Permutation_app_comm; auto. Qed.
imports: List ListAux