proposition: Lemma similar_ulblockmx n1 n2 n3 (Aul : 'M[R]_n1) (Adr : 'M[R]_n3) (Bul : 'M[R]_n2) : similar Aul Bul -> similar (block_mx Aul 0 0 Adr) (block_mx Bul 0 0 Adr).
proof: Proof. case=> Hn1 [P HP HAB]. have Hu : (block_mx P 0 0 1%:M) \in unitmx. by move=> n; rewrite unitmxE det_ublock det1 mulr1 -unitmxE. split; first by rewrite Hn1. move: Aul P HP HAB Hu; rewrite Hn1=> Aul P HP; rewrite conform_mx_id=> HAB Hu. exists (block_mx P 0 0 1%:M); 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