proposition: Lemma poly_ind (K : {poly R} -> Type) : K 0 -> (forall p c, K p -> K (p * 'X + c%:P)) -> (forall p, K p).
proof: Proof. move=> K0 Kcons p; rewrite -[p]polyseqK. by elim: {p}(p : seq R) => //= p c IHp; rewrite cons_poly_def; apply: Kcons. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype bigop finset tuple) mathcomp(div ssralg countalg binomial)