proposition: Lemma lem_perm_1 {A} : forall (x y : A) l1 l2 l3, Permutation l1 (y :: l2) -> Permutation (x :: l1 ++ l3) (y :: x :: l2 ++ l3).
proof: Proof. srun eauto use: @lem_perm_0, perm_skip, Permutation_Add, Permutation_trans, Permutation_sym, perm_swap unfold: app. Undo. srun eauto use: @lem_perm_0, Permutation_trans, perm_swap. Qed.
imports: Hammer(Hammer) Arith Sorting.Permutation