proposition: Lemma Fadjoin_polyX : x \notin K -> Fadjoin_poly K x x = 'X.
proof: Proof. move=> K'x; apply: Fadjoin_poly_unique; rewrite ?polyOverX ?hornerX //. by rewrite size_polyX ltn_neqAle andbT eq_sym adjoin_deg_eq1. 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)