proposition: Fact subfx_scalerDl x : {morph subfx_scale^~ x : a b / a + b}.
proof: Proof. by move=> a b; rewrite /subfx_scale rmorphD mulrDl. 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)