proposition: Lemma root_size_gt1 a p : p != 0 -> root p a -> 1 < size p.
proof: Proof. rewrite ltnNge => nz_p; apply: contraL => /size1_polyC Dp. by rewrite Dp rootC -polyC_eq0 -Dp. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype bigop finset tuple) mathcomp(div ssralg countalg binomial)