proposition: Lemma scale_mxvec a m n (M : 'M[R]_(m,n)) : a *: mxvec M = mxvec (a *: M).
proof: Proof. apply/matrixP=> i j; rewrite mxE ord1 {i}. by case/mxvec_indexP: j=> i j; rewrite !mxvecE mxE. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq path) mathcomp(ssralg fintype perm choice fingroup) mathcomp(matrix bigop zmodp mxalgebra poly) ssrcomplements