proposition: Lemma upper_triangular_mx0 m n : upper_triangular_mx (0 : 'M[R]_(m,n)).
proof: Proof. by apply/upper_triangular_mxP=> i j; rewrite mxE. 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