proposition: Lemma perm_cat2r s1 s2 s3 : perm (s2 ++ s1) (s3 ++ s1) <-> perm s2 s3.
proof: Proof. split; last by apply: perm_cat2rL. elim: s1 s2 s3=>[|x s1 IH] s2 s3 /=; first by rewrite !cats0. by move=>H; apply: IH; apply: perm_cat_consR H. Qed.
imports: mathcomp(ssreflect ssrfun seq) LemmaOverloading(rels)