proposition: Lemma adjoin_numfield_roots (p : {poly rat}) : (<<1 & numfield_roots p>> = fullv)%VS.
proof: Proof. rewrite /numfield_roots; case: eqP => [p0|/negP]; first by case: sig2_eqW. by rewrite negbK => /eqP->; rewrite numfield0 regular_fullv Fadjoin_nil. 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)