proposition: Lemma lalgMixin (R : ringType) (A : lalgType R) (B : lmodType R) (f : B -> A) : phant B -> injective f -> scalable f -> forall mulB, {morph f : x y / mulB x y >-> x * y} -> forall a u v, a *: (mulB u v) = mulB (a *: u) v.
proof: Proof. by move=> _ injf fZ mulB fM a x y; apply: injf; rewrite !(fZ, fM) scalerAl. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop prime binomial)