proposition: Lemma gen_tperm_step n (k : 'I_n.+2) : coprime n.+2 k -> <<[set tperm i (i + k) | i : 'I_n.+2]>>%g = [set: 'S_n.+2].
proof: Proof. rewrite -unitZpE// natr_Zp => k_unit. apply/eqP; rewrite eqEsubset subsetT/= -(gen_tperm 0)/= gen_subG. apply/subsetP => s /imsetP[/= i _ ->]. rewrite -[i](mulVKr k_unit) -[_ * i]natr_Zp mulr_natr. elim: (val _) => //= {i} [|[|i] IHi]; first by rewrite tperm1 group1. by rewrite mulrSr mem_gen//; apply/imsetP; exists 0. have [->|kS2N0] := eqVneq (k *+ i.+2) 0; first by rewrite tperm1 group1. have kSSneqkS : k *+ i.+2 != k *+ i.+1. rewrite -subr_eq0 -mulrnBr// subSnn mulr1n. by apply: contraTneq k_unit => ->; rewrite unitr0. rewrite -(@tpermJt _ (k *+ i.+1)) 1?eq_sym//. rewrite groupJ// 1?tpermC// mulrSr 1?tpermC. by rewrite mem_gen//; apply/imsetP; exists (k *+ i.+1). Qed.
imports: HB(structures) mathcomp(all_ssreflect all_fingroup all_algebra all_solvable) mathcomp(all_field)