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