proposition: Lemma pet_alg_proof (s : seq alg) : { ap : {alg F} * seq {poly F} | [forall i : 'I_(size s), (ap.2`_i ^ to_alg).[ap.1] == s`_i] & size ap.2 = size s }.
proof: Proof. apply: sig2_eqW; elim: s; first by exists (0,[::])=> //; apply/forallP=> [] []. move=> x s [[a sp] /forallP /= hs hsize]. have:= char0_PET _ (root_annul_alg a) _ (root_annul_alg x). rewrite !annul_alg_neq0 => /(_ isT isT (char_num _)) /= [n [[p hp] [q hq]]]. exists (x *+ n - a, q :: [seq r \Po p | r <- sp]); last first. by rewrite /= size_map hsize. apply/forallP=> /=; rewrite -add1n=> i; apply/eqP. have [k->|l->] := splitP i; first by rewrite !ord1. rewrite add1n /= (nth_map 0) ?hsize // map_comp_poly /=. by rewrite horner_comp hp; apply/eqP. Qed.
imports: HB(structures) mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq choice fintype) mathcomp(bigop order ssralg ssrnum ssrint rat poly polydiv polyorder) mathcomp(perm matrix mxpoly polyXY binomial generic_quotient) mathcomp(cauchyreals separable zmodp bigenough)