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