proposition: Lemma char_block_mx m n (A : 'M[R]_m) (D : 'M[R]_n) B C : char_poly_mx (block_mx A B C D) = block_mx (char_poly_mx A) (map_mx polyC (-B)) (map_mx polyC (-C)) (char_poly_mx D).
proof: Proof. apply/matrixP=> i j; rewrite !mxE. case: splitP=> k eqik; rewrite !mxE; case: splitP=> l eqjmpl; rewrite !mxE; rewrite -!(inj_eq (@ord_inj _)) eqik eqjmpl ?eqn_add2l // rmorphN. by rewrite ltn_eqF ?ltn_addr // sub0r. by rewrite gtn_eqF ?ltn_addr // sub0r. Qed.
imports: mathcomp(all_ssreflect all_algebra)