proposition: Fact subfx_scalerA a b x : subfx_scale a (subfx_scale b x) = subfx_scale (a * b) x.
proof: Proof. by rewrite /subfx_scale rmorphM mulrA. 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)