proposition: Lemma abstrXP (i : nat) (t : tF) (e : seq F) (x : F) : rterm t -> (eval_poly e (abstrX i t)).[x] = eval (set_nth 0 e i x) t.
proof: Proof. elim: t => [n | r | n | t tP s sP | t tP | t tP n | t tP s sP | t tP | t tP n] h. - move=> /=; case ni: (_ == _); rewrite //= ?(mul0r,add0r,addr0,polyC1,mul1r,hornerX,hornerC); by rewrite // nth_set_nth /= ni. - by rewrite /= mul0r add0r hornerC. - by rewrite /= mul0r add0r hornerC. - by case/andP: h => *; rewrite /= eval_sumpT hornerD tP ?sP. - by rewrite /= eval_opppT hornerN tP. - by rewrite /= eval_natmulpT hornerMn tP. - by case/andP: h => *; rewrite /= eval_mulpT hornerM tP ?sP. - by []. - elim: n h => [|n ihn] rt; first by rewrite /= expr0 mul0r add0r hornerC. by rewrite /= eval_mulpT exprSr hornerM ihn // mulrC tP. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype choice ssrnat seq) mathcomp(fintype generic_quotient bigop ssralg poly) mathcomp(polydiv matrix mxpoly countalg ring_quotient)