proposition: Lemma classic_fieldExtFor (F0 : fieldType) (L : fieldExtType F0) (p : {poly L}) : p != 0 -> classically { L' : fieldExtType F0 & { rs : seq L' & { iota : 'AHom(L, L') | <<iota @: fullv & rs>>%VS = fullv & p ^^ iota %= \prod_(r <- rs) ('X - r%:P) }}}.
proof: Proof. have [n] := ubnP (size p); elim: n => [|n IHn]// in F0 L p *. rewrite ltnS => sp_lt p_neq0. apply: classic_bind (@classic_EM (irreducible_poly p)) => -[]; last first. have [|p_gt1] := leqP (size p) 1. rewrite leq_eqVlt ltnS leqn0 size_poly_eq0 (negPf p_neq0) orbF. move=> /size_poly1P[c cN0 ->] _. apply/classicW; exists L, [::], (id_ahom _). by rewrite Fadjoin_nil/= lim1g. by rewrite big_nil map_polyC/= lfunE/= polyC_eqp1. move=> NNred_p; have: classically (exists q : {poly L}, [/\ size q != 1%N, (size q < size p)%N & q %| p]). apply/classicP => Nexq; apply: NNred_p. split => // q sq_neq1 dvdqp; apply: contraTT isT => eq_qp. case: Nexq; exists q; split => //. by rewrite ltn_neqAle dvdp_size_eqp// eq_qp/= dvdp_leq. apply: classic_bind => -[q [qN1 sq qp]]. have qN0 : q != 0 by apply: contraTneq qp => ->; rewrite dvd0p. have sqn : (size q < n)%N by rewrite (leq_trans sq). apply: classic_bind (IHn _ _ _ sqn qN0) => -[L1 [rs1 [iota1 rs1_full qE]]]. have /dvdpP [r pE]:= qp. have rN0 : r != 0 by apply: contra_eq_neq pE => ->; rewrite mul0r. have r1N0 : r ^^ iota1 != 0 by rewrite map_poly_eq0. have srn : (size (r ^^ iota1) < n)%N. rewrite size_map_poly. have /(congr1 (fun p : {poly _} => size p)) := pE. rewrite size_mul// [size q]polySpred// addnS/=. move=> /(canLR (@addnK _))<-; rewrite (leq_trans _ sp_lt)//. rewrite ltn_subrL size_poly_gt0 p_neq0 andbT. by rewrite ltn_predRL// ltn_neqAle eq_sym qN1 ?size_poly_gt0/=. apply: classic_bind (IHn _ _ _ srn r1N0) => -[L2 [rs2 [iota2 rs2_full rE]]]. apply/classicW; exists L2, (map iota2 rs1 ++ rs2), (iota2 \o iota1)%AF. by rewrite adjoin_cat limg_comp -aimg_adjoin_seq rs1_full rs2_full. rewrite big_cat/= big_map (eq_map_poly (comp_lfunE _ _)) map_poly_comp pE. rewrite !rmorphM/= mulrC (eqp_trans (eqp_mull _ rE))// eqp_mulr//. have := qE; rewrite -(eqp_map iota2) => /eqp_trans->//=. rewrite (big_morph _ (rmorphM _) (rmorph1 _))/=. under eq_bigr do rewrite rmorphB/= -/iota map_polyX map_polyC/=. by rewrite eqpxx. move=> /irredp_FAdjoin[L1 df [r1 r1_root r1_full]]. pose L01 : fieldExtType F0 := baseFieldType L1. pose r01 : L01 := r1. pose inL01 : L -> L01 := in_alg L1. have iotam : multiplicative inL01. by split; [exact: rmorphM|rewrite /inL01 rmorph1]. have iotal : scalable inL01. by move=> k a; rewrite /inL01 -mulr_algl rmorphM/= mulr_algl. pose iotaaM := GRing.isAdditive.Build _ _ inL01 (rmorphB _). pose iotamM := GRing.isMultiplicative.Build _ _ inL01 iotam. pose iotalM := GRing.isScalable.Build _ _ _ _ inL01 iotal. pose iotaLRM : {lrmorphism _ -> _} := HB.pack inL01 iotaaM iotamM iotalM. pose iota1 : 'AHom(L, L01) := AHom (linfun_is_ahom iotaLRM). have inL01E : inL01 =1 iota1 by move=> x; rewrite lfunE. have r01_root : root (p ^^ iota1) r01 by rewrite -(eq_map_poly inL01E). have r01_full : <<limg iota1; r01>>%VS = fullv. apply/eqP; rewrite eqEsubv subvf/=; apply/subvP => v _. have : (v : L1) \in <<1; r1>>%VS by rewrite r1_full memvf. move/Fadjoin_polyP => [pr pr1 ->]. suff [qr ->] : exists2 qr, pr = qr & qr \is a polyOver (limg iota1). exact: mempx_Fadjoin. have /polyOver1P[qr ->] := pr1; exists (map_poly iota1 qr). by apply/eq_map_poly => w; rewrite lfunE. by apply/polyOverP => i; rewrite coef_map/= memv_img ?memvf. have /dvdpP[q pE] : ('X - r01%:P) %| (p ^^ iota1) by rewrite dvdp_XsubCl. have qN0 : q != 0. by apply: contra_eq_neq pE => ->; rewrite mul0r map_poly_eq0//. have sq : (size q < n)%N. have /(congr1 (fun p : {poly _} => size p)) := pE. rewrite size_map_poly size_mul ?polyXsubC_eq0//. by rewrite size_XsubC addn2//= => <-. apply: classic_bind (IHn _ _ _ sq qN0) => -[L2 [rs2 [iota12 rs2_full qE]]]. apply/classicW. exists L2, (iota12 r01 :: rs2), (iota12 \o iota1)%AF. by rewrite adjoin_cons limg_comp -aimg_adjoin r01_full rs2_full. rewrite big_cons/= (eq_map_poly (comp_lfunE _ _)) map_poly_comp pE. by rewrite rmorphM/= mulrC rmorphB/= map_polyX map_polyC/= eqp_mull. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_fingroup all_algebra) mathcomp(all_solvable all_field) Abel(various cyclotomic_ext)