proposition: Lemma pperm_sym s1 s2 : perm s1 s2 <-> perm s2 s1.
proof: Proof. suff {s1 s2} L : forall s1 s2, perm s1 s2 -> perm s2 s1 by split; apply: L. apply: perm_ind=>[|||??? _ H1 _ H2] *; by [apply: permutation_nil | apply: permutation_skip | apply: permutation_swap | apply: permutation_trans H2 H1]. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat seq path eqtype) pcm(options pred)