proposition: Lemma similar_drblockmx n1 n2 n3(Aul : 'M[R]_n1) (Adr : 'M[R]_n2) (Bdr : 'M[R]_n3) : similar Adr Bdr -> similar (block_mx Aul 0 0 Adr) (block_mx Aul 0 0 Bdr).
proof: Proof. case=> Hn2 [P HP HAB]. have Hu : (block_mx 1%:M 0 0 P) \in unitmx. by move=> n; rewrite unitmxE det_ublock det1 mul1r -unitmxE. split; first by rewrite Hn2. move: Adr P HP HAB Hu; rewrite Hn2=> Adr P HP; rewrite conform_mx_id=> HAB Hu. exists (block_mx 1%:M 0 0 P); first exact: Hu. rewrite conform_mx_id !mulmx_block !mul0mx !mulmx0. by rewrite !add0r !addr0 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