proposition: Lemma mulmx_delta_companion (R : ringType) (p : seq R) (i: 'I_(size p).-1) (i_small : i.+1 < (size p).-1): delta_mx 0 i *m companionmx p = delta_mx 0 (Ordinal i_small) :> 'rV__.
proof: Proof. apply/rowP => j; rewrite !mxE (bigD1 i) //= ?(=^~val_eqE, mxE) /= eqxx mul1r. rewrite ltn_eqF ?big1 ?addr0 1?eq_sym //; last first. by rewrite -ltnS prednK // (leq_trans _ i_small). by move=> k /negPf ki_eqF; rewrite !mxE eqxx ki_eqF mul0r. 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)