proposition: Lemma ratr_p_over : map_poly (ratr : rat -> L) p \is a polyOver 1%AS.
proof: Proof. apply/polyOverP => i; rewrite -char0_ratrE coef_map /=. by rewrite char0_ratrE -alg_num_field rpredZ ?mem1v. 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)