proposition: Lemma pperm_nil (s : seq A) : perm [::] s <-> s = [::].
proof: Proof. split; last by move=>->; apply: permutation_nil. move E: {1}[::]=>l H; move: H {E}(esym E). by elim=>//??? _ IH1 _ IH2 /IH1/IH2. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat seq path eqtype) pcm(options pred)