proposition: Lemma tens_row_mx {m n p q} (r : 'cV[R]_m) (M :'M[R]_(m,n)) (N : 'M[R]_(p,q)) : (row_mx r M) *t N = castmx (erefl _, esym (mulnDl _ _ _)) (row_mx (r *t N) (M *t N)).
proof: Proof. rewrite -[_ *t _]trmxK trmx_tens tr_row_mx tens_col_mx. apply/eqP; rewrite -(can2_eq (castmxKV _ _) (castmxK _ _)); apply/eqP. by rewrite trmx_cast castmx_comp castmx_id tr_col_mx -!trmx_tens !trmxK. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq choice fintype) mathcomp(bigop ssralg matrix zmodp div)