proposition: Lemma polyC_eq0 (c : R) : (c%:P == 0) = (c == 0).
proof: Proof. by rewrite -nil_poly polyseqC; case: (c == 0). Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype bigop finset tuple) mathcomp(div ssralg countalg binomial)