proposition: Lemma eval_poly_mulM e : {morph eval_poly e : x y / mulpT x y >-> x * y}.
proof: Proof. by move=> x y; rewrite eval_mulpT. 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)