proposition: Lemma pet_algK s i : ((pet_alg_poly s)`_i ^ to_alg).[pet_alg s] = s`_i.
proof: Proof. rewrite /pet_alg /pet_alg_poly; case: pet_alg_proof. move=> [a sp] /= /forallP hs hsize; have [lt_is|le_si] := ltnP i (size s). by rewrite -[i]/(val (Ordinal lt_is)); apply/eqP; apply: hs. by rewrite !nth_default ?hsize // rmorph0 horner0. 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)