proposition: Lemma perm_catC s1 s2 : perm (s1 ++ s2) (s2 ++ s1).
proof: Proof. elim:s1 s2=>[|x s1 IH1] s2 /=; first by rewrite cats0. apply: (@perm_trans (x::s2++s1)); first by apply: permutation_skip (IH1 s2). elim: s2=>[|y s2 IH2] //=. apply: (@perm_trans (y::x::s2++s1)); first by apply: permutation_swap eq_refl. by apply: permutation_skip IH2. Qed.
imports: mathcomp(ssreflect ssrfun seq) LemmaOverloading(rels)