proposition: Lemma subfx_inj_root : subfx_inj subfx_root = z.
proof: Proof. by rewrite subfx_inj_eval // map_polyX hornerX. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq div) mathcomp(choice fintype tuple finfun bigop ssralg countalg) mathcomp(finalg zmodp matrix vector falgebra poly polydiv) mathcomp(mxpoly generic_quotient)