proposition: Lemma abstrXP e i t x : (eval_poly e (abstrX i t)).[x] = eval (set_nth 0 e i x) t.
proof: Proof. elim: t. - move=> n /=; case ni: (_ == _); rewrite //= ?(mul0r,add0r,addr0,polyC1,mul1r,hornerX,hornerC); by rewrite // nth_set_nth /= ni. - by move=> r; rewrite /= mul0r add0r hornerC. - by move=> r; rewrite /= mul0r add0r hornerC. - by move=> t tP s sP; rewrite /= eval_AddPoly hornerD tP ?sP. - by move=> t tP; rewrite /= eval_OppPoly hornerN tP. - by move=> t tP n; rewrite /= eval_NatMulPoly hornerMn tP. - by move=> t tP s sP; rewrite /= eval_MulPoly hornerM tP ?sP. - by move=> t tP n; rewrite /= eval_ExpPoly horner_exp tP. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq choice fintype) mathcomp(finfun path matrix) mathcomp(bigop order ssralg poly polydiv ssrnum zmodp div ssrint) mathcomp(polyorder polyrcf interval polyXY) mathcomp(qe_rcf_th ordered_qelim mxtens)