proposition: Lemma mulmx_is_bilinear (R : comRingType) m n p : bilinear_for (GRing.Scale.Law.clone _ _ *:%R _) (GRing.Scale.Law.clone _ _ *:%R _) (@mulmx R m n p).
proof: Proof. split=> [u'|u] a x y /=. - by rewrite mulmxDl scalemxAl. - by rewrite mulmxDr scalemxAr. Qed.
imports: HB(structures) mathcomp(all_ssreflect ssralg fingroup zmodp poly ssrnum) mathcomp(matrix mxalgebra vector falgebra ssrnum algC algnum) mathcomp(fieldext) mathcomp(vector)