proposition: Lemma equiv_dgblockmx m1 n1 m2 n2 m3 n3 m4 n4 (Aul : 'M[R]_(m1,n1)) (Adr : 'M[R]_(m2,n2)) (Bul : 'M[R]_(m3,n3)) (Bdr : 'M[R]_(m4,n4)) : equivalent Aul Bul -> equivalent Adr Bdr -> equivalent (block_mx Aul 0 0 Adr) (block_mx Bul 0 0 Bdr).
proof: Proof. move=> HABu HABd; apply: (equiv_trans (B:=(block_mx Bul 0 0 Adr))). exact: equiv_ulblockmx. exact: equiv_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