proposition: Lemma gen_tpermn_cycle n (i j : 'I_n.+2) (c := perm (addrI 1)) : coprime n.+2 (j - i)%R -> <<[set tperm i j ; c]>>%g = [set: 'S_n.+2].
proof: Proof. move=> jBi_coprime; apply/eqP; rewrite eqEsubset subsetT/=. rewrite -(gen_tperm_step jBi_coprime) gen_subG. apply/subsetP => s /imsetP[/= k _ ->]. suff -> : tperm k (k + (j - i)) = (tperm i j ^ c ^+ (k - i)%R)%g. by rewrite groupJ ?groupX ?mem_gen ?inE ?eqxx ?orbT. by rewrite tpermJ !perm_add1X addrNK addrAC addrA. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_fingroup all_algebra all_solvable) mathcomp(all_field)