proposition: Lemma char_poly_mx_triangular_mx n (M : 'M[R]_n) : upper_triangular_mx M -> upper_triangular_mx (char_poly_mx M).
proof: Proof. move/upper_triangular_mxP=> HM; apply/upper_triangular_mxP=>i j Hij. rewrite !mxE. suff /negbTE->/=: i != j by rewrite (HM i j Hij) GRing.subr0. by move: Hij; rewrite ltn_neqAle eq_sym; case/andP. 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