proposition: Lemma cycleij_inS i (j k : 'I_n) : i <= k < j -> 's_[index_iota i j] (inord k.+1) = k.
proof: Proof. rewrite /index_iota => /andP[lejk ltkj]. have ltij := leq_ltn_trans lejk ltkj. have lekj := ltnW ltkj. have -> /= : iota i (j - i) = iota i (k - i) ++ iota k (j - k.+1).+1. rewrite subnS prednK ?subn_gt0 //. suff -> : (j - i) = (k - i) + (j - k) by rewrite iotaD subnKC. by rewrite addnC addnBA // subnK. rewrite big_cat /= big_cons permM cycleij_gt //; first last. by rewrite inordK // ltnS (leq_trans ltkj) // -ltnS. rewrite permM eltrR_ord. have Hk1 := inordK (leq_ltn_trans ltkj (ltn_ord _)). by rewrite -Hk1 cycleij_lt // Hk1. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(fingroup perm morphism presentation) mathcomp(ssralg poly ssrint) permcomp tools permuted combclass congr