proposition: Lemma block_mx_eq0 m1 m2 n1 n2 (Aul : 'M_(m1, n1)) Aur Adl (Adr : 'M_(m2, n2)) : (block_mx Aul Aur Adl Adr == 0) = [&& Aul == 0, Aur == 0, Adl == 0 & Adr == 0].
proof: Proof. by rewrite col_mx_eq0 !row_mx_eq0 !andbA. 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)