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