proposition: Lemma tensmx0 {m n p q} (M : 'M[R]_(m,n)) : M *t (0 : 'M_(p,q)) = 0.
proof: Proof. by apply/matrixP=> i j; rewrite !mxE mulr0. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq choice fintype) mathcomp(bigop ssralg matrix zmodp div)