proposition: Fact CtoL_P u : integralOver QtoL (CtoL u).
proof: Proof. rewrite /CtoL /rootQtoL; case: (repr u) => p j /=. case: (closed_field_poly_normal _) => r Dp /=. case: ifPn => [_ | nz_p]; first exact: integral0. have [/(nth_default 0)-> | lt_j_r] := leqP (size r) j; first exact: integral0. apply/integral_algebraic; exists p; rewrite // Dp -mul_polyC rootM orbC. by rewrite root_prod_XsubC mem_nth. 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)