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