proposition: Lemma perm_catL s1 t1 s2 t2 : perm s1 s2 -> perm t1 t2 -> perm (s1 ++ t1) (s2 ++ t2).
proof: Proof. move=>H; move: s1 s2 H t1 t2; apply: perm_ind=>s1 s2. - by move=>->->. - move=>x t1 t2 -> -> H IH r1 r2. by move/IH; apply: permutation_skip. - move=>x y t -> -> t1 t2 H. by apply: (permutation_trans (t:=[:: x, y & t] ++ t2)); [apply: perm_cat2lL | simpl; apply: permutation_swap eq_refl]. move=>t H1 IH1 H2 IH2 t1 t2 H. by apply: permutation_trans (IH2 _ _ H); apply: IH1. Qed.
imports: mathcomp(ssreflect ssrfun seq) LemmaOverloading(rels)