proposition: Lemma Fadjoin_polyC v : v \in K -> Fadjoin_poly K x v = v%:P.
proof: Proof. move=> Kv; apply: Fadjoin_poly_unique; rewrite ?polyOverC ?hornerC //. by rewrite size_polyC (leq_trans (leq_b1 _)). 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)