proposition: Lemma Fadjoin_poly_mod p : p \is a polyOver K -> Fadjoin_poly K x p.[x] = p %% minPoly K x.
proof: Proof. move=> Kp; rewrite {1}(divp_eq p (minPoly K x)) 2!hornerE minPolyxx mulr0 add0r. apply: Fadjoin_poly_unique => //; first by rewrite modp_polyOver // minPolyOver. by rewrite -ltnS -size_minPoly ltn_modp // monic_neq0 ?monic_minPoly. 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)