proposition: Lemma similar_dgblockmx n1 n2 n3 n4 (Aul : 'M[R]_n1) (Adr : 'M[R]_n2) (Bul : 'M[R]_n3) (Bdr : 'M[R]_n4) : similar Aul Bul -> similar Adr Bdr -> similar (block_mx Aul 0 0 Adr) (block_mx Bul 0 0 Bdr).
proof: Proof. move=> HABu HABd; apply: (similar_trans (B:= (block_mx Bul 0 0 Adr))). exact: similar_ulblockmx. exact: similar_drblockmx. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype fintype finfun ssrnat seq) mathcomp(choice ssralg poly polydiv mxpoly matrix bigop) mathcomp(mxalgebra perm fingroup tuple) mxstructure dvdring