proposition: Lemma cycleij_gt (i j : nat) (k : 'I_n) : j < k -> 's_[index_iota i j] k = k.
proof: Proof. Proof using. move=> ltij; rewrite big_seq; elim/big_ind: _. - by rewrite perm1. - by move=> s t Hs Ht; rewrite permM Hs Ht. move=> u; rewrite mem_iota => /andP[leiu]. case: (ltnP j i) => [/ltnW |]. rewrite -subn_eq0 => /eqP ->. by rewrite addn0 => /leq_trans/(_ leiu); rewrite ltnn. move=> /subnKC -> /leq_ltn_trans/(_ ltij) ltu1k. have u1o := ltn_trans ltu1k (ltn_ord k). have uo := ltn_trans (ltnSn _) u1o. rewrite eltrD // -val_eqE //= inordK // ltn_eqF //. exact: (ltn_trans (ltnSn _) ltu1k). Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(fingroup perm morphism presentation) mathcomp(ssralg poly ssrint) permcomp tools permuted combclass congr