proposition: Lemma upper_triangular_block : upper_triangular_mx Aul -> upper_triangular_mx Adr -> m1 <= n1 -> upper_triangular_mx (block_mx Aul 0 0 Adr).
proof: Proof. move=> /upper_triangular_mxP HAul /upper_triangular_mxP HAdr H. apply/upper_triangular_mxP=> i j Hij; rewrite !mxE. case: splitP=> k Hk; rewrite !mxE; case: splitP=> l Hl; rewrite ?mxE //. by apply: HAul; rewrite -Hk -Hl. apply: HAdr; rewrite -(ltn_add2l m1) -Hk. rewrite Hl in Hij; apply: (leq_ltn_trans _ Hij). by rewrite leq_add2r. 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