proposition: Lemma equiv_ulblockmx m1 n1 m2 n2 m3 n3 (Aul : 'M[R]_(m1,n1)) (Adr : 'M[R]_(m2,n2)) (Bul : 'M[R]_(m3,n3)) : equivalent Aul Bul -> equivalent (block_mx Aul 0 0 Adr) (block_mx Bul 0 0 Adr).
proof: Proof. case=> eqm eqn [M [N [HM HN HAB]]]. split; rewrite ?eqm ?eqn //. move: Aul M N HM HN HAB; rewrite eqm eqn => Aul M N HM HN. rewrite !conform_mx_id=> HAB. exists (block_mx M 0 0 1%:M), (block_mx N 0 0 1%:M). split; try by rewrite unitmxE det_ublock det1 mulr1 -unitmxE. by rewrite !mulmx_block !mulmx0 !mul0mx !addr0 !mul0mx !add0r mulmx1 mul1mx HAB. 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