proposition: Lemma Fadjoin_poly_unique p v : p \is a polyOver K -> size p <= n -> p.[x] = v -> Fadjoin_poly K x v = p.
proof: Proof. have polyKx q i: q \is a polyOver K -> q`_i * x ^+ i \in (K * <[x ^+ i]>)%VS. by move/polyOverP=> Kq; rewrite memv_mul ?Kq ?memv_line. move=> Kp szp Dv; have /Fadjoin_poly_eq/eqP := mempx_Fadjoin Kp. rewrite {1}Dv {Dv} !(@horner_coef_wide _ n) ?size_poly //. move/polyKx in Kp; have /polyKx K_pv := Fadjoin_polyOver K x v. rewrite (directv_sum_unique Fadjoin_sum_direct) // => /eqfunP eq_pq. apply/polyP=> i; have [leni|?] := leqP n i; last exact: mulIf (eq_pq (Sub i _)). by rewrite !nth_default ?(leq_trans _ leni) ?size_poly. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq div) mathcomp(choice fintype tuple finfun bigop ssralg countalg) mathcomp(finalg zmodp matrix vector falgebra poly polydiv) mathcomp(mxpoly generic_quotient)