proposition: Lemma block_mxA m1 m2 m3 n1 n2 n3 (A11 : 'M_(m1, n1)) (A12 : 'M_(m1, n2)) (A13 : 'M_(m1, n3)) (A21 : 'M_(m2, n1)) (A22 : 'M_(m2, n2)) (A23 : 'M_(m2, n3)) (A31 : 'M_(m3, n1)) (A32 : 'M_(m3, n2)) (A33 : 'M_(m3, n3)) : let cast := (esym (addnA m1 m2 m3), esym (addnA n1 n2 n3)) in let row1 := row_mx A12 A13 in let col1 := col_mx A21 A31 in let row3 := row_mx A31 A32 in let col3 := col_mx A13 A23 in block_mx A11 row1 col1 (block_mx A22 A23 A32 A33) = castmx cast (block_mx (block_mx A11 A12 A21 A22) col3 row3 A33).
proof: Proof. rewrite /= block_mxEh !col_mxA -cast_row_mx -block_mxEv -block_mxEh. rewrite block_mxEv block_mxEh !row_mxA -cast_col_mx -block_mxEh -block_mxEv. by rewrite castmx_comp etrans_id. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype finfun bigop finset fingroup perm order) mathcomp(div prime binomial ssralg countalg finalg zmodp)