proposition: Lemma upper_triangular_block_mxul : upper_triangular_mx (block_mx Aul Aur Adl Adr) -> upper_triangular_mx Aul.
proof: Proof. move=> /upper_triangular_mxP HA; apply/upper_triangular_mxP=> i j Hij. by rewrite -(HA (lshift m2 i) (lshift n2 j)) ?block_mxEul. 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