proposition: Lemma perm_iotaP {s t : seq T} x0 (It := iota 0 (size t)) : reflect (exists2 Is, perm_eq Is It & s = map (nth x0 t) Is) (perm_eq s t).
proof: Proof. apply: (iffP idP) => [Est | [Is eqIst ->]]; last first. by rewrite -{2}[t](mkseq_nth x0) perm_map. elim: t => [|x t IHt] in s It Est *. by rewrite (perm_small_eq _ Est) //; exists [::]. have /rot_to[k s1 Ds]: x \in s by rewrite (perm_mem Est) mem_head. have [|Is1 eqIst1 Ds1] := IHt s1; first by rewrite -(perm_cons x) -Ds perm_rot. exists (rotr k (0 :: map succn Is1)). by rewrite perm_rot /It /= perm_cons (iotaDl 1) perm_map. by rewrite map_rotr /= -map_comp -(@eq_map _ _ (nth x0 t)) // -Ds1 -Ds rotK. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)