proposition: Lemma eval_poly1 e : eval_poly e [::1%T] = 1.
proof: Proof. by rewrite /= mul0r add0r. 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)