proposition: Lemma companion_map_poly (e := esym (congr1 predn (size_map_poly _ _))) : companionmx (fp p) = castmx (e, e) (companionmx p)^f.
proof: Proof. by rewrite map_mx_companion castmx_comp castmx_id. 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)