proposition: Lemma dvd_dG : (d %| #|'Gal(K / 1%VS)%g|)%N.
proof: Proof. rewrite dim_fixedField (galois_fixedField _) ?galois1K ?dimv1 ?divn1//. rewrite (@dvdn_trans (\dim_(1%VS : {vspace L}) <<1; rp`_0>>%VS))//. rewrite -adjoin_degreeE -[X in (_ %| X)%N]/(_.+1.-1). rewrite -size_minPoly (eqp_size (minPoly_rp _)) ?mem_nth ?size_rp//. by rewrite -char0_ratrE size_map_poly. rewrite dimv1 divn1 K_eq field_dimS//= -adjoin_seq1 adjoin_seqSr//. have: (0 < size rp)%N by rewrite size_rp. by case: rp => //= x l _ y; rewrite inE => /eqP->; rewrite inE eqxx. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_fingroup all_algebra) mathcomp(all_solvable all_field polyrcf) Abel(various classic_ext map_gal algR) Abel(char0 cyclotomic_ext real_closed_ext)