proposition: Lemma lem_perm_2 : forall (x : nat) l1 l2 l3, Permutation (x :: l1) l2 -> Permutation (x :: l3 ++ l1) (l3 ++ l2).
proof: Proof. srun eauto use: Permutation_app_head, Permutation_trans, Permutation_app_comm, Permutation_cons_app. Qed.
imports: Hammer(Hammer) Arith Sorting.Permutation