proposition: Lemma perm_cons_cat_consL s1 s2 s x : perm s (s1 ++ s2) -> perm (x :: s) (s1 ++ x :: s2).
proof: Proof. case: s1=>[|a s1] /= H; first by apply: permutation_skip H. apply: (@perm_trans (x::a::s1++s2)); first by apply: permutation_skip eq_refl H. apply: (@perm_trans (a::x::s1++s2)); first by apply: permutation_swap eq_refl. by apply: permutation_skip eq_refl eq_refl _=>//. Qed.
imports: mathcomp(ssreflect ssrfun seq) LemmaOverloading(rels)