proposition: Lemma coef1 i : (1 : {poly R})`_i = (i == 0)%:R.
proof: Proof. by case: i => [|i]; rewrite polyseq1 /= ?nth_nil. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype bigop finset tuple) mathcomp(div ssralg countalg binomial)