proposition: Theorem Permutation_transposition : forall (a b : A) l1 l2, Permutation (a :: l1 ++ b :: l2) (b :: l1 ++ a :: l2).
proof: Proof. intros a b l1 l2. assert (H_eq: b :: l1 ++ a :: l2 = (b :: l1) ++ a :: l2) by reflexivity. rewrite H_eq. apply Permutation_cons_app. apply Permutation_sym. apply Permutation_cons_app; auto. Qed.
imports: Coq(Inverse_Image Wf_nat Sorting.Permutation)