proposition: Lemma lem_perm_4 : forall (x y : nat) l1 l2 l3, Permutation (x :: l1) l2 -> Permutation (x :: y :: l3 ++ l1) (y :: l3 ++ l2).
proof: Proof. intros. rewrite List.app_comm_cons. pattern (y :: l3 ++ l2). rewrite List.app_comm_cons. apply lem_perm_2; assumption. Qed.
imports: Hammer(Hammer) Arith Sorting.Permutation