proposition: Lemma conjL_rp : {mono conjL : x / x \in rp}.
proof: Proof. suff rpJ : {homo conjL : x / x \in rp}. by move=> x; apply/idP/idP => /rpJ//; rewrite conjLK. move=> ?/(nthP 0)[i]; rewrite size_rp => ltid <-. rewrite -!root_p -!topredE /root/=. have /eq_map_poly<- : conjL \o char0_ratr charL =1 _ := fmorph_eq_rat _. by rewrite map_poly_comp horner_map ratr_p_rp ?rmorph0. 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)