proposition: Lemma pperm_cons_cat_cons x s1 s2 s : perm (x :: s) (s1 ++ x :: s2) <-> perm s (s1 ++ s2).
proof: Proof. by split; [apply: (@pperm_cat_consR [::]) | apply: pperm_cons_cat_consL]. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat seq path eqtype) pcm(options pred)