proposition: Theorem permutation_app_swap : forall l1 l2, permutation (l1 ++ l2) (l2 ++ l1).
proof: Proof. intros l1; elim l1; auto. intros; rewrite <- app_nil_end; auto. intros a l H l2. replace (l2 ++ a :: l) with ((l2 ++ a :: nil) ++ l). apply permutation_trans with (l ++ l2 ++ a :: nil); auto. apply permutation_trans with (((a :: nil) ++ l2) ++ l); auto. simpl in |- *; auto. apply permutation_trans with (l ++ (a :: nil) ++ l2); auto. apply permutation_sym; auto. replace (l2 ++ a :: l) with ((l2 ++ a :: nil) ++ l). apply permutation_app_comp; auto. elim l2; simpl in |- *; auto. intros a0 l0 H0. apply permutation_trans with (a0 :: a :: l0); auto. apply (app_ass l2 (a :: nil) l). apply (app_ass l2 (a :: nil) l). Qed.
imports: List ListAux