proposition: Lemma ratr_example_poly : poly_example ^^ ratr = \prod_(x <- example_roots) ('X - x%:P).
proof: Proof. rewrite /example_roots -map_prod_XsubC/=. have := poly_numfield_eqp poly_example_neq0. rewrite eqp_monic ?monic_prod_XsubC ?monic_map// => /eqP<-. by rewrite -map_poly_comp [in RHS](eq_map_poly (fmorph_eq_rat _)). 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)