proposition: Lemma similar_poly m n (A : 'M[R]_m.+1) (B : 'M_n.+1) p: similar A B -> similar (horner_mx A p) (horner_mx B p).
proof: Proof. case=> /eqP; rewrite eqSS=> /eqP eq [P HP]; move: B. rewrite /similar -eq=> B; rewrite conform_mx_id=> HAB. split=> //; exists P => //; rewrite conform_mx_id. elim/poly_ind: p=>[|p c IHp]. by rewrite !rmorph0 mulmx0 mul0mx. rewrite !rmorphD !rmorphM /= !horner_mx_X !horner_mx_C. by rewrite mulmxDr mulmxDl mulmxA IHp -mulmxA HAB mulmxA scalar_mxC. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype fintype finfun ssrnat seq) mathcomp(choice ssralg poly polydiv mxpoly matrix bigop) mathcomp(mxalgebra perm fingroup tuple) mxstructure dvdring