proposition: Lemma gen_tperm (X : finType) x : <<[set tperm x y | y in X]>>%g = [set: {perm X}].
proof: Proof. apply/eqP; rewrite eqEsubset subsetT/=; apply/subsetP => s _. have [ts -> _] := prod_tpermP s; rewrite group_prod// => -[/= y z] _. have [<-|Nyz] := eqVneq y z; first by rewrite tperm1 group1. have [<-|Nxz] := eqVneq x z; first by rewrite tpermC mem_gen ?imset_f. by rewrite -(tpermJt Nxz Nyz) groupJ ?mem_gen ?imset_f. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_fingroup all_algebra all_solvable) mathcomp(all_field)