proposition: Lemma Jordan_expn (lam : R) n k : (Jordan_block lam n.+1)^+ k = \matrix_(i,j) (('C(k,j - i)%:R * (lam^+ (k - (j - i)))) *+ (i <= j)).
proof: Proof. elim: k =>[|k IHk]. apply/matrixP=> i j; rewrite !mxE bin0n subn_eq0 sub0n mulr1 [RHS]mulrb. by rewrite -(inj_eq (@ord_inj _)) eqn_leq /andb; case: ifP. rewrite exprS IHk. apply/matrixP=> i j; rewrite !mxE. case: (eqVneq i ord_max) => Hi. - rewrite (bigD1 i) //= !mxE big1 ?addr0=>[|l /negbTE Hl]. - rewrite eqxx eqn_leq ltnn addr0. have ->: (j - i)%N = 0%N by apply/eqP; rewrite subn_eq0 Hi -ltnS. by rewrite !bin0 !mul1r !subn0 mulrnAr exprS. rewrite !mxE eq_sym [(_ == _ :> nat)]Hl Hi eqn_leq. by rewrite ltnNge -ltnS ltn_ord addr0 mul0r. have Ho: (i.+1 < n.+1)%N by rewrite ltn_neqAle Hi ltn_ord. rewrite (bigD1 i) //= (bigD1 (Ordinal Ho)); last first. by rewrite -(inj_eq (@ord_inj _)) eqn_leq ltnn. rewrite !mxE eqxx (@eq_sym nat i) !eqn_leq !ltnn addr0 add0r. rewrite !leqnn mul1r subnS /= big1 ?addr0; last first. move=> l /andP [] /negbTE Hil /negbTE Hl. by rewrite !mxE eq_sym [_ == _ :>nat]Hil eq_sym [_ == _ :>nat]Hl addr0 mul0r. case: (ltngtP i j)=> Hij; last first. - by rewrite Hij subnn !subn0 addr0 !bin0 !mul1r exprS. - by rewrite addr0 mulr0. rewrite !mulr1n mulrC -mulrA -exprSr -{2}subn1. have H1ij: (1 <= j - i)%N by rewrite subn_gt0. rewrite (subnBA _ H1ij) addn1. case: (leqP (j-i) k)=> Hijk. by rewrite (subSn Hijk) -mulrDl -{1}(prednK H1ij) -natrD -binS prednK. have:= Hijk; rewrite -subn_eq0=> /eqP Hijk2. rewrite (bin_small Hijk) // mul0r Hijk2 !mulr1 add0r. rewrite leq_eqVlt in Hijk. case/orP: Hijk=> Hijk. rewrite (eqP Hijk) binn. rewrite -(prednK H1ij) eqSS in Hijk. by rewrite (eqP Hijk) binn. by rewrite !bin_small // -ltnS prednK. 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)