proposition: Lemma horner_mx_mem p : (horner_mx A p \in Ad)%MS.
proof: Proof. elim/poly_ind: p => [|p a IHp]; first by rewrite rmorph0 // linear0 sub0mx. rewrite rmorphD rmorphM /= horner_mx_C horner_mx_X. rewrite addrC -scalemx1 linearP /= -(mul_vec_lin (mulmxr A)). case/submxP: IHp => u ->{p}. have: (powers_mx A (1 + d) <= Ad)%MS. rewrite -(geq_leqif (mxrank_leqif_sup _)). by rewrite (eqnP minpoly_mx_free) /d; case: ex_minnP. rewrite addnC; apply/row_subP=> i. by apply: eq_row_sub (lshift 1 i) _; rewrite !rowK. apply: submx_trans; rewrite addmx_sub ?scalemx_sub //. by apply: (eq_row_sub 0); rewrite rowK. rewrite -mulmxA mulmx_sub {u}//; apply/row_subP=> i. rewrite row_mul rowK mul_vec_lin /= mulmxE -exprSr. by apply: (eq_row_sub (rshift 1 i)); rewrite rowK. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat choice seq) mathcomp(div fintype tuple finfun bigop fingroup perm) mathcomp(ssralg zmodp matrix mxalgebra poly polydiv)