proposition: Lemma perm_consP x s t : reflect (exists i u, rot i t = x :: u /\ perm_eq u s) (perm_eq t (x :: s)).
proof: Proof. apply: (iffP idP) => [eq_txs | [i [u [Dt eq_us]]]]. have /rot_to[i u Dt]: x \in t by rewrite (perm_mem eq_txs) mem_head. by exists i, u; rewrite -(perm_cons x) -Dt perm_rot. by rewrite -(perm_rot i) Dt perm_cons. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)