proposition: Corollary eltr_genSn : 'SG_n = <<[set 's_(i : 'I_n0) | i in 'I_n0]>>%G.
proof: Proof. apply/setP => s; apply/idP/gen_prodgP => /=. - move=> Hs; exists (size (canword s)). exists (fun i => 's_(tnth (in_tuple (canword s)) i)). + by move=> i; apply: imset_f. + rewrite -{1}(canwordP s). by rewrite -{1}[canword s]/(tval (in_tuple (canword s))) big_tuple. - move=> [l [fi Hfi] ->{s}]; apply group_prod => i _. by rewrite inE. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(fingroup perm morphism presentation) mathcomp(ssralg poly ssrint) permcomp tools permuted combclass congr