proposition: Lemma tens_block_mx {m n p q} (ul : 'M[R]_1) (ur : 'rV[R]_n) (dl : 'cV[R]_m) (M :'M[R]_(m,n)) (N : 'M[R]_(p,q)) : (block_mx ul ur dl M) *t N = castmx (esym (mulnDl _ _ _), esym (mulnDl _ _ _)) (block_mx (ul *t N) (ur *t N) (dl *t N) (M *t N)).
proof: Proof. rewrite !block_mxEv tens_col_mx !tens_row_mx -!cast_col_mx castmx_comp. by congr (castmx (_,_)); apply nat_irrelevance. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq choice fintype) mathcomp(bigop ssralg matrix zmodp div)