proposition: Lemma NhornerE (R : comRingType) N (env : seq R) (p : Npoly [comRingType of int] N) : Nhorner env p = (@NhornerR _ _) env (Nmap_poly intr p).
proof: Proof. by rewrite /Nhorner; case: horner_key. 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)