proposition: Lemma gen_tperm01_cycle n (c := perm (addrI 1)) : <<[set tperm 0 1%R ; c]>>%g = [set: 'S_n.+2].
proof: Proof. by rewrite gen_tpermn_cycle// subr0 coprimen1. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_fingroup all_algebra all_solvable) mathcomp(all_field)