proposition: Lemma cycleij_lt (i j k : 'I_n) : i <= j -> k < i -> 's_[index_iota i j] k = k.
proof: Proof. Proof using. move=> leij ltki; rewrite /index_iota -{1}(subKn leij). by apply: prods_iota_ltmi; rewrite subKn. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(fingroup perm morphism presentation) mathcomp(ssralg poly ssrint) permcomp tools permuted combclass congr