proposition: Lemma root_small_adjoin_poly p : p \is a polyOver K -> size p <= n -> root p x = (p == 0).
proof: Proof. move=> Kp szp; apply/rootP/eqP=> [px0 | ->]; last by rewrite horner0. rewrite -(Fadjoin_poly_unique Kp szp px0). by apply: Fadjoin_poly_unique; rewrite ?polyOver0 ?size_poly0 ?horner0. 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)