proposition: Lemma upt_Jordan_block lam n : upper_triangular_mx (Jordan_block lam n).
proof: Proof. apply/upper_triangular_mxP=> i j Hij ; rewrite mxE. by rewrite (gtn_eqF Hij) eqn_leq ltnNge (ltnW Hij) addr0. Qed.
imports: mathcomp(all_ssreflect) mathcomp(all_algebra) mathcomp(all_fingroup) mathcomp(all_real_closed) CoqEAL(binetcauchy ssrcomplements mxstructure minor) CoqEAL(smith dvdring polydvd) CoqEAL(similar perm_eq_image companion closed_poly smith_complements) CoqEAL(frobenius_form)