proposition: Lemma row'_col'_triangular_mx n (M : 'M[R]_n) i: upper_triangular_mx M -> upper_triangular_mx (row' i (col' i M)).
proof: Proof. move/upper_triangular_mxP=> HM; apply/upper_triangular_mxP=> j k Hij. rewrite !mxE HM // /lift /= /bump /ltn -addn1 -addnA addn1. apply: leq_add=> //; case H: (i <= k)=> //=. by rewrite (ltnW (leq_ltn_trans H Hij)). 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