proposition: Lemma algebraic : integralRange (@ratr type).
proof: Proof. move=> u; have [p mon_p pu0] := CtoL_P u; exists p => {mon_p}//. rewrite -(fmorph_root CtoL) -map_poly_comp; congr (root _ _):pu0. by apply/esym/eq_map_poly; apply: fmorph_eq_rat. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun ssrnat eqtype seq choice) mathcomp(div fintype path bigop finset prime order ssralg) mathcomp(poly polydiv mxpoly generic_quotient countalg) mathcomp(ssrnum closed_field ssrint archimedean rat intdiv) mathcomp(algebraics_fundamentals)