proposition: Lemma permutationsErot x s (le_x := fun t => iota 0 (index x t + 1)) : perm_eq (perms (x :: s)) [seq rot i (x :: t) | t <- perms s, i <- le_x t].
proof: Proof. have take'x t i: i <= index x t -> i <= size t /\ x \notin take i t. move=> le_i_x; have le_i_t: i <= size t := leq_trans le_i_x (index_size x t). case: (nthP x) => // -[j lt_j_i /eqP]; rewrite size_takel // in lt_j_i. by rewrite nth_take // [_ == _](before_find x (leq_trans lt_j_i le_i_x)). pose xrot t i := rot i (x :: t); pose xrotV t := index x (rev (rot 1 t)). have xrotK t: {in le_x t, cancel (xrot t) xrotV}. move=> i; rewrite mem_iota addn1 /xrotV => /take'x[le_i_t ti'x]. rewrite -rotD ?rev_cat //= rev_cons cat_rcons index_cat mem_rev size_rev. by rewrite ifN // size_takel //= eqxx addn0. apply/uniq_perm=> [||t]; first exact: permutations_uniq. apply/allpairs_uniq_dep=> [|t _|]; rewrite ?permutations_uniq ?iota_uniq //. move=> _ _ /allpairsPdep[t [i [_ ? ->]]] /allpairsPdep[u [j [_ ? ->]]] Etu. have Eij: i = j by rewrite -(xrotK t i) // /xrot Etu xrotK. by move: Etu; rewrite Eij => /rot_inj[->]. rewrite mem_permutations; apply/esym; apply/allpairsPdep/idP=> [[u [i]] | Dt]. rewrite mem_permutations => -[Du _ /(canLR (rotK i))]; rewrite /rotr. by set j := (j in rot j _) => Dt; apply/perm_consP; exists j, u. pose r := rev (rot 1 t); pose i := index x r; pose u := rev (take i r). have r_x: x \in r by rewrite mem_rev mem_rot (perm_mem Dt) mem_head. have [v Duv]: {v | rot i (x :: u ++ v) = t}; first exists (rev (drop i.+1 r)). rewrite -rev_cat -rev_rcons -rot1_cons -cat_cons -(nth_index x r_x). by rewrite -drop_nth ?index_mem // rot_rot !rev_rot revK rotK rotrK. exists (u ++ v), i; rewrite mem_permutations -(perm_cons x) -(perm_rot i) Duv. rewrite mem_iota addn1 ltnS /= index_cat mem_rev size_rev. by have /take'x[le_i_t ti'x] := leqnn i; rewrite ifN ?size_takel ?leq_addr. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)