proposition: Lemma num_field_exists (s : seq algC) : {Qs : fieldExtType rat & {QsC : {rmorphism Qs -> algC} & {s1 : seq Qs | map QsC s1 = s & <<1 & s1>>%VS = fullv}}}.
proof: Proof. have [z /sig_eqW[a Dz] /sig_eqW[ps Ds]] := algC_PET s. suffices [Qs [QsC [z1 z1C z1gen]]]: {Qs : fieldExtType rat & {QsC : {rmorphism Qs -> algC} & {z1 : Qs | QsC z1 = z & forall xx, exists p, fieldExt_horner z1 p = xx}}}. - set inQs := fieldExt_horner z1 in z1gen *; pose s1 := map inQs ps. have inQsK p: QsC (inQs p) = (pQtoC p).[z]. rewrite /= -horner_map z1C -map_poly_comp; congr _.[z]. apply: eq_map_poly => b /=; apply: canRL (mulfK _) _. by rewrite intr_eq0 denq_eq0. rewrite /= mulrzr -rmorphMz scalerMzl -{1}[b]divq_num_den -mulrzr. by rewrite divfK ?intr_eq0 ?denq_eq0 // scaler_int rmorph_int. exists Qs, QsC, s1; first by rewrite -map_comp Ds (eq_map inQsK). have sz_ps: size ps = size s by rewrite Ds size_map. apply/vspaceP=> x; rewrite memvf; have [p {x}<-] := z1gen x. elim/poly_ind: p => [|p b ApQs]; first by rewrite /inQs rmorph0 mem0v. rewrite /inQs rmorphD rmorphM /= fieldExt_hornerX fieldExt_hornerC -/inQs /=. suffices ->: z1 = \sum_(i < size s) s1`_i *+ a i. rewrite memvD ?memvZ ?mem1v ?memvM ?memv_suml // => i _. by rewrite rpredMn ?seqv_sub_adjoin ?mem_nth // size_map sz_ps. apply: (fmorph_inj QsC); rewrite z1C Dz rmorph_sum; apply: eq_bigr => i _. by rewrite rmorphMn {1}Ds !(nth_map 0) ?sz_ps //= inQsK. have [r [Dr /monic_neq0 nz_r] dv_r] := minCpolyP z. have rz0: root (pQtoC r) z by rewrite dv_r. have irr_r: irreducible_poly r. by apply/(subfx_irreducibleP rz0 nz_r)=> q qz0 nzq; rewrite dvdp_leq // -dv_r. exists (SubFieldExtType rz0 irr_r), (@subfx_inj _ _ QtoC z r). exists (subfx_root _ z r) => [|x]; first exact: subfx_inj_root. by have{x} [p ->] := subfxEroot rz0 nz_r x; exists p. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(div choice fintype tuple finfun bigop prime) mathcomp(ssralg poly polydiv ssrnum ssrint archimedean rat) mathcomp(finalg zmodp matrix mxalgebra mxpoly vector intdiv) mathcomp(falgebra fieldext separable galois algC cyclotomic)