proposition: Lemma sizeY_poly_ground p : sizeY (poly_ground p) = size p.
proof: Proof. unlock poly_ground; rewrite sizeYE swapXYK; have [->|p_neq0] := eqVneq p 0. apply/eqP; rewrite size_poly0 eqn_leq leq0n (leq_trans (size_Poly _)) //. by rewrite size_pet_alg_poly size_poly0. rewrite (@PolyK _ 0) -?nth_last ?size_pet_alg_poly //. have /eqP := (pet_algK p (size p).-1); apply: contraL=> /eqP->. by rewrite rmorph0 horner0 -lead_coefE eq_sym lead_coef_eq0. 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)