proposition: Lemma polyficationP (R : comRingType) (env : seq R) N p : size env == N -> PExpr_to_Expr env p = Nhorner env (PExpr_to_poly N p).
proof: Proof. elim: p=> [n|n|p IHp q IHq|p IHp q IHq|p IHp|p IHp n] /=. - by rewrite NhornerE !rmorph_int. - rewrite NhornerE; elim: N env n=> [|N IHN] [|a env] [|n] //= senv. by rewrite map_polyX hornerX [RHS]NhornerRC. by rewrite map_polyC hornerC !IHN. - by move=> senv; rewrite (IHp senv) (IHq senv) !NhornerE !rmorphD. - by move=> senv; rewrite (IHp senv) (IHq senv) !NhornerE !rmorphM. - by move=> senv; rewrite (IHp senv) !NhornerE !rmorphN. - by move=> senv; rewrite (IHp senv) !NhornerE !rmorphX. 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)