proposition: Lemma upper_triangular_mxP m n {M : 'M_(m,n)} : reflect (forall (i : 'I_m) (j : 'I_n), j < i -> M i j = 0) (upper_triangular_mx M).
proof: Proof. apply/(iffP eqP)=> [H i j Hij|H]. rewrite /upper_triangular_mx in H. by rewrite H mxE leqNgt Hij. apply/matrixP => i j; rewrite mxE leqNgt. by case/boolP: (j < i) => // /H ->. 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