proposition: Lemma horner_coef0 p : p.[0] = p`_0.
proof: Proof. by rewrite /horner; case: (p : seq R) => //= c p'; rewrite !simp. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype bigop finset tuple) mathcomp(div ssralg countalg binomial)