proposition: Lemma perm_eq_perm (A : eqType) (s1 s2 : seq A) : reflect (perm s1 s2) (perm_eq s1 s2).
proof: Proof. apply: (iffP idP); last first. - elim=>[|||??? _ H1 _ H2]*. - by apply seq.perm_refl. - by rewrite seq.perm_cons. - by rewrite -![[:: _, _ & _]]/([::_] ++ [::_] ++ _) seq.perm_catCA; rewrite !seq.perm_cat2l. by apply: seq.perm_trans H1 H2. elim: s2 s1 =>[s1 /seq.perm_size/size0nil->// | x s2 IH s1 H]. move: (seq.perm_mem H x); rewrite mem_head=>H'; move: H' H. move/splitPr=>[p1 p2]; rewrite -cat1s seq.perm_catCA seq.perm_cons=>/IH. by rewrite -[_::s2]cat0s pperm_cat_cons. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat seq path eqtype) pcm(options pred)