proposition: Lemma permPl s1 s2 : reflect (perm_eql s1 s2) (perm_eq s1 s2).
proof: Proof. apply: (iffP idP) => [eq12 s3 | -> //]; apply/idP/idP; last exact: perm_trans. by rewrite -!(perm_sym s3) => /perm_trans; apply. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)