proposition: Lemma subfx_eval_is_multiplicative : multiplicative subfx_eval.
proof: Proof. split=> [x y|]; apply/eqP; rewrite piE. by rewrite /subfx_mul_rep !poly_rV_modp_K !(modp_mul, mulrC _ y). by rewrite modp_small // size_poly1 -subn_gt0 subn1. 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)