proposition: Lemma similar_horner n m (A : 'M[R]_n.+1) (B : 'M_m.+1) p : similar A B -> horner_mx A p = 0 -> horner_mx B p = 0.
proof: Proof. move/(similar_poly p)=> HAB HhA; move: HAB; rewrite HhA. case=> /eqP; rewrite eqSS=> /eqP eq [P HP]. rewrite -eq in B *; rewrite conform_mx_id mulmx0=> H. by apply: (mulIr HP); rewrite mul0r. 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