proposition: Lemma is_diag_block_mx m1 m2 n1 n2 ul ur dl dr : m1 = n1 -> @is_diag_mx (m1 + m2) (n1 + n2) (block_mx ul ur dl dr) = [&& ur == 0, dl == 0, is_diag_mx ul & is_diag_mx dr].
proof: Proof. move=> eq_m1_n1. rewrite !is_diag_mxEtrig tr_block_mx !is_trig_block_mx// trmx_eq0. by rewrite andbACA -!andbA; congr [&& _, _, _ & _]; rewrite andbCA. 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)