proposition: Lemma poly_groundK p : ((poly_ground p) ^ (map_poly to_alg)).[(pet_alg p)%:P] = p.
proof: Proof. have [->|p_neq0] := eqVneq p 0; first by rewrite poly_ground0 rmorph0 horner0. unlock poly_ground; rewrite horner_polyC /eval /= swapXY_map swapXYK. apply/polyP=> i /=; rewrite coef_map_id0 ?horner0 // coef_map /=. by rewrite coef_Poly pet_algK. 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)