proposition: Lemma algC_invaut_subproof nu x : {y | nu y = x}.
proof: Proof. have [r Dp] := closed_field_poly_normal (minCpoly x). suffices /mapP/sig2_eqW[y _ ->]: x \in map nu r by exists y. rewrite -root_prod_XsubC; congr (root _ x): (root_minCpoly x). have [q [Dq _] _] := minCpolyP x; rewrite Dq -(eq_map_poly (fmorph_rat nu)). rewrite (map_poly_comp nu) -{q}Dq Dp (monicP (minCpoly_monic x)) scale1r. rewrite rmorph_prod big_map /=; apply: eq_bigr => z _. by rewrite rmorphB /= map_polyX map_polyC. 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)