proposition: Lemma mx_inv_horner0 : mx_inv_horner 0 = 0.
proof: Proof. by rewrite /mx_inv_horner !(linear0, mul0mx). 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)