proposition: Lemma algC_PET (s : seq algC) : {z | exists a : nat ^ size s, z = \sum_(i < size s) s`_i *+ a i & exists ps, s = [seq (pQtoC p).[z] | p <- ps]}.
proof: Proof. elim: s => [|x s [z /sig_eqW[a Dz] /sig_eqW[ps Ds]]]. by exists 0; [exists [ffun _ => 2%N]; rewrite big_ord0 | exists nil]. have r_exists (y : algC): {r | r != 0 & root (pQtoC r) y}. have [r [_ mon_r] dv_r] := minCpolyP y. by exists r; rewrite ?monic_neq0 ?dv_r. suffices /sig_eqW[[n [|px [|pz []]]]// [Dpx Dpz]]: exists np, let zn := x *+ np.1 + z in [:: x; z] = [seq (pQtoC p).[zn] | p <- np.2]. - exists (x *+ n + z). exists [ffun i => oapp a n (unlift ord0 i)]. rewrite /= big_ord_recl ffunE unlift_none Dz; congr (_ + _). by apply: eq_bigr => i _; rewrite ffunE liftK. exists (px :: [seq p \Po pz | p <- ps]); rewrite /= -Dpx; congr (_ :: _). rewrite -map_comp Ds; apply: eq_map => p /=. by rewrite map_comp_poly horner_comp -Dpz. have [rx nz_rx rx0] := r_exists x. have [rz nz_rz rz0] := r_exists (- z). have char0_Q: [char rat] =i pred0 by apply: char_num. have [n [[pz Dpz] [px Dpx]]] := char0_PET nz_rz rz0 nz_rx rx0 char0_Q. by exists (n, [:: px; - pz]); rewrite /= !raddfN hornerN -[z]opprK Dpz Dpx. 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)