proposition: Fact minCpoly_subproof (x : algC) : {p : {poly rat} | p \is monic & forall q, root (pQtoC q) x = (p %| q)%R}.
proof: Proof. have isQ := rat_algebraic_decidable algebraic. have [p [mon_p px0 irr_p]] := minPoly_decidable_closure isQ (algebraic x). exists p => // q; apply/idP/idP=> [qx0 | /dvdpP[r ->]]; last first. by rewrite rmorphM rootM px0 orbT. suffices /eqp_dvdl <-: gcdp p q %= p by apply: dvdp_gcdr. rewrite irr_p ?dvdp_gcdl ?gtn_eqF // -(size_map_poly QtoC) gcdp_map /=. rewrite (@root_size_gt1 _ x) ?root_gcd ?px0 //. by rewrite gcdp_eq0 negb_and map_poly_eq0 monic_neq0. 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)