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