Permutation with firstn and skipn

Using Coq
1

I’ve been struggling with this part of a proof because of the firstn and skipn part.

Permutation (x :: a :: a0 :: l)
(firstn (length (a :: a0 :: l) / 2) (a :: a0 :: l) ++
x :: skipn (length (a :: a0 :: l) / 2) (a :: a0 :: l))

2

You can simplify your theorem: the a :: a0 :: l is immaterial.

Permutation (x :: l0)
            (firstn (length l0 / 2) l0 ++
             x :: skipn (length l0 / 2) l0)

The specific length is also irrelevant:

Permutation (x :: l0) (firstn n l0 ++ x :: skipn n l0)

From there you should be able Permutation and List lemmas to finish the proof.