proposition: Lemma PolyK c s : last c s != 0 -> Poly s = s :> seq R.
proof: Proof. case: s => {c}/= [_ |c s]; first by rewrite polyseqC eqxx. elim: s c => /= [|a s IHs] c nz_c; rewrite polyseq_cons ?{}IHs //. by rewrite !polyseqC !eqxx nz_c. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype bigop finset tuple) mathcomp(div ssralg countalg binomial)