proposition: Lemma roots_geq_poly_eq0 p (rs : seq R) : all (root p) rs -> uniq rs -> (size rs >= size p)%N -> p = 0.
proof: Proof. by move=> ??; apply: contraTeq => ?; rewrite leqNgt max_poly_roots. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype bigop finset tuple) mathcomp(div ssralg countalg binomial)