proposition: Lemma upper_triangular_block_mxdl : upper_triangular_mx (block_mx Aul Aur Adl Adr) -> n1 <= m1 -> Adl = 0.
proof: Proof. move=> HA Hn1. apply/matrixP=> i j. transitivity (block_mx Aul Aur Adl Adr (rshift m1 i) (lshift n2 j)). by rewrite block_mxEdl. rewrite (upper_triangular_mxP HA) ?mxE //=. by apply/ltn_addr/(leq_trans (ltn_ord j)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq path) mathcomp(ssralg fintype perm poly mxpoly finfun tuple) mathcomp(matrix bigop zmodp polydiv) ssrcomplements dvdring