proposition: Lemma example_not_solvable_by_radicals : ~ solvable_by_radical_poly ('X^5 - 4 *: 'X + 2 : {poly rat}).
proof: Proof. move=> /AbelGaloisPolyRat; pose sol_gal := isog_sol (PDTNRR.isog_gal _ _ _). rewrite sol_gal ?size_poly_example ?solvable_SymF ?card_ord//. by rewrite -(count_map _ [predC Creal]) count_roots_ex. 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)