proposition: Lemma perm_cat2rL s s1 s2 : perm s1 s2 -> perm (s1 ++ s) (s2 ++ s).
proof: Proof. move=>H; move: s1 s2 H s; apply: perm_ind=>s1 s2. - by move=>->->. - by move=>x t1 t2 -> -> H IH s /=; apply: permutation_skip (IH _). - by move=>x y t -> -> s /=; apply: permutation_swap eq_refl. by move=>t H1 IH1 H2 IH2 s; apply: permutation_trans (IH2 s). Qed.
imports: mathcomp(ssreflect ssrfun seq) LemmaOverloading(rels)