proposition: Lemma lem_perm_0 {A} : forall (x y : A) l1 l2 l3, Permutation l1 (y :: l2) -> Permutation (x :: l1 ++ l3) (x :: y :: l2 ++ l3).
proof: Proof. hauto lq: on drew: off use: Permutation_app, List.app_comm_cons, Permutation_refl, perm_skip. Qed.
imports: Hammer(Hammer) Arith Sorting.Permutation