proposition: Lemma pperm_cat2r s s1 s2 : perm (s1 ++ s) (s2 ++ s) <-> perm s1 s2.
proof: Proof. split; last by apply: pperm_cat2rL. by elim: s=>[|??? /pperm_cat_consR]; rewrite ?cats0. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat seq path eqtype) pcm(options pred)