proposition: Lemma sizeTP (pf : polyF) : sizeT pf ->_e size (eval_poly e pf).
proof: Proof. elim: pf=> [|c qf qfP /=]; first by rewrite /= size_poly0. move=> e k; rewrite size_MXaddC qfP -(size_poly_eq0 (eval_poly _ _)). by case: (size (eval_poly e qf))=> //=; case: eqP; rewrite // orbF. 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)