proposition: Lemma Fadjoin_polyOver v : Fadjoin_poly v \is a polyOver U.
proof: Proof. apply/(all_nthP 0) => i _; rewrite coef_poly /=. case: ifP => lti; last exact: mem0v. have /memv_cosetP[y Uy ->] := memv_sum_pi (erefl Fadjoin_sum) (inord i) v. rewrite inordK //; have [-> | /mulfK-> //] := eqVneq (x ^+ i) 0. by rewrite mulr0 mul0r mem0v. 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)