proposition: Lemma perm_cat2l s1 s2 s3: perm (s1 ++ s2) (s1 ++ s3) <-> perm s2 s3.
proof: Proof. split; last by apply: perm_cat2lL. elim: s1 s2 s3=>[|x s1 IH] s2 s3 //= H. by apply: IH; move/perm_cons: H. Qed.
imports: mathcomp(ssreflect ssrfun seq) LemmaOverloading(rels)