proposition: Lemma cycleij_in i (j k : 'I_n) : i < k <= j -> 's_[index_iota i j] k = (inord k.-1).
proof: Proof. move=> /andP[ltik lekj]. have eqk1 : val k = (inord k.-1 : 'I_n).+1. by rewrite inordK ?(ltn_predK ltik) // ltnW. rewrite -{1}(inord_val k) {1}eqk1 cycleij_inS //. by rewrite -ltnS -eqk1 ltik. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(fingroup perm morphism presentation) mathcomp(ssralg poly ssrint) permcomp tools permuted combclass congr