proposition: Lemma root_ZXsubC (a b r : F) : a != 0 -> root (a *: 'X - b%:P) r = (r == b / a).
proof: Proof. move=> a0; rewrite rootE !hornerE. by rewrite -[r in RHS]divr1 eqr_div ?oner_neq0// mulr1 mulrC subr_eq0. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype bigop finset tuple) mathcomp(div ssralg countalg binomial)