proposition: Lemma NhornerRS (R : comRingType) N (a : R) (env : seq R) (p : Npoly R N.+1) : NhornerR (a :: env) p = NhornerR env p.[NpolyC N a].
proof: Proof. by elim: N p. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq ssralg ssrint) mathcomp(path choice fintype tuple finset ssralg bigop poly polydiv) mathcomp(zmodp) CoqEAL(hrel param refinements binint poly_op hpoly karatsuba)