proposition: Lemma horner_mx_stable (K : fieldType) m n p (V : 'M[K]_(n.+1, m.+1)) (f : 'M_m.+1) : stablemx V f -> stablemx V (horner_mx f p).
proof: Proof. move=> V_fstab; elim/poly_ind: p => [|p c]; first by rewrite rmorph0 stablemx0. move=> fp_stable; rewrite rmorphD rmorphM/= horner_mx_X horner_mx_C. by rewrite stablemxD ?stablemxM ?fp_stable ?stablemxC. 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)