proposition: Fact subfx_inj_is_multiplicative : multiplicative subfx_inj.
proof: Proof. split; last by rewrite piE /iotaFz poly_rV_K ?rmorph1 ?size_poly1. elim/quotW=> x; elim/quotW=> y; rewrite !piE /subfx_mul_rep /iotaFz. by rewrite poly_rV_modp_K iotaPz_modp rmorphM. 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)