proposition: Lemma upper_triangular_block_mxdr : upper_triangular_mx (block_mx Aul Aur Adl Adr) -> n1 <= m1 -> upper_triangular_mx Adr.
proof: Proof. move=> /upper_triangular_mxP HA Hn1; apply/upper_triangular_mxP=> i j Hij. rewrite -(HA (rshift m1 i) (rshift n1 j)) ?block_mxEdr // -addnS. exact: leq_add. 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