proposition: Lemma perm_cons2 (x y : A) s : perm_eq [:: x, y & s] [:: y, x & s].
proof: Proof. by rewrite (_ : [::x,y & s] = [::x] ++ [::y] ++ s) // (_ : [::y,x & s] = [::y] ++ [::x] ++ s) // perm_catCA. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat seq eqtype path fintype finfun tuple interval perm fingroup) pcm(options prelude ordtype seqext slice)