proposition: Lemma pperm_cat2lL s s1 s2 : perm s1 s2 -> perm (s ++ s1) (s ++ s2).
proof: Proof. by elim: s=>[//|e s IH /IH]; apply: permutation_skip. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat seq path eqtype) pcm(options pred)