proposition: Lemma char_dblock_mx m n (A : 'M[R]_m) (B : 'M[R]_n) : char_poly_mx (block_mx A 0 0 B) = block_mx (char_poly_mx A) 0 0 (char_poly_mx B).
proof: Proof. by rewrite char_block_mx !oppr0 !map_mx0. Qed.
imports: mathcomp(all_ssreflect all_algebra)