proposition: Lemma Jordan_block0 : Jordan_block 0 1 = 0.
proof: Proof. by apply/matrixP=> i j; rewrite !mxE !ord1 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)