proposition: Lemma diag_mx_row m n (l : 'rV_n) (r : 'rV_m) : diag_mx (row_mx l r) = block_mx (diag_mx l) 0 0 (diag_mx r).
proof: Proof. apply/matrixP => i j. by do ?[rewrite !mxE; case: split_ordP => ? ->]; rewrite mxE eq_shift. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype finfun bigop finset fingroup perm order) mathcomp(div prime binomial ssralg countalg finalg zmodp)