proposition: Fact horner_is_linear : linear_for (f \; *%R) (horner_morph cfu).
proof: Proof. by move=> c p q; rewrite /horner_morph rmorphD /= hornerD linearZ hornerZ. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype bigop finset tuple) mathcomp(div ssralg countalg binomial)