proposition: Lemma horner_mx_diag_block (p : {poly R}) s F : s != [::] -> horner_mx (diag_block_mx s F) p = diag_block_mx s (fun n i => horner_mx (F n i) p).
proof: Proof. case: s=> // x s _. elim/poly_ind: p. rewrite rmorph0; apply: esym; apply/diag_block_mx0=> // i _. by rewrite rmorph0. move=> p c IHp. set s1 := _ :: _. set F1 := fun n i => _ _ (_ + _). pose F2 := fun n i => horner_mx (F n i) p *m (F n i) + horner_mx (F n i) c%:P. have Hi: forall i, i < size s1 -> F1 (nth 0%N s1 i) i = F2 (nth 0%N s1 i) i. by move=> i _; rewrite /F1 /F2 rmorphD rmorphM /= horner_mx_X. rewrite (ext_block Hi) /F2 -add_diag_block -mulmx_diag_block. rewrite rmorphD rmorphM /=. rewrite horner_mx_X horner_mx_C IHp. set F3 := fun n i => _ _ c%:P. rewrite -(@scalar_diag_block_mx _ c (x :: s) F3) // => i Hi2. by rewrite /F3 horner_mx_C. 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