proposition: Fact LtoC_subproof z : integralOver QtoL z -> {u | CtoL u = z}.
proof: Proof. case/sig2_eqW=> p mon_p pz0; rewrite /CtoL. pose j := index z (sval (closed_field_poly_normal (pQtoL p))). pose u := \pi_type%qT (p, j); exists u; have /eqmodP/eqP-> := reprK u. rewrite /rootQtoL -if_neg monic_neq0 //; apply: nth_index => /=. case: (closed_field_poly_normal _) => r /= Dp. by rewrite Dp (monicP _) ?(monic_map QtoL) // scale1r root_prod_XsubC in pz0. 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)