proposition: Lemma pperm_cat2rL s s1 s2 : perm s1 s2 -> perm (s1 ++ s) (s2 ++ s).
proof: Proof. move=>?. apply: (@pperm_trans (s ++ s1)); first by apply: pperm_catC. apply: (@pperm_trans (s ++ s2)); last by apply: pperm_catC. by apply: pperm_cat2lL. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat seq path eqtype) pcm(options pred)