proposition: Fact Fadjoin_poly_is_linear : linear_for (in_alg L \; *:%R) Fadjoin_poly.
proof: Proof. move=> a u v; apply/polyP=> i; rewrite coefD coefZ !coef_poly. case: ifP => lti; last by rewrite mulr0 addr0. by rewrite linearP mulrA -mulrDl mulr_algl. 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)