proposition: Lemma map_mx_companion (e := congr1 predn (size_map_poly _ _)) : (companionmx p)^f = castmx (e, e) (companionmx (fp p)).
proof: Proof. apply/matrixP => i j; rewrite !(castmxE, mxE) /= (fun_if f). by rewrite rmorphN coef_map size_map_poly rmorph_nat. 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)