proposition: Lemma eval_lift (e : seq F) (p : {poly F}) : eval_poly e (lift p) = p.
proof: Proof. elim/poly_ind: p => [|p c]; first by rewrite /lift polyseq0. rewrite -cons_poly_def /lift polyseq_cons /nilp. case pn0: (_ == _) => /=; last by move->; rewrite -cons_poly_def. move=> _; rewrite polyseqC. case c0: (_==_)=> /=. move: pn0; rewrite (eqP c0) size_poly_eq0; move/eqP->. by apply: val_inj=> /=; rewrite polyseq_cons // polyseq0. by rewrite mul0r add0r; apply: val_inj=> /=; rewrite polyseq_cons // /nilp pn0. 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)