proposition: Lemma eval_Size k p e : qf_eval e (Size p k) = qf_eval e (k (size (eval_poly e p))).
proof: Proof. elim: p e k=> [|c p ihp] e k; first by rewrite size_poly0. rewrite ihp /= size_MXaddC -size_poly_eq0; case: size=> //. by rewrite eval_If /=; case: (_ == _). Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq choice fintype) mathcomp(finfun path matrix) mathcomp(bigop order ssralg poly polydiv ssrnum zmodp div ssrint) mathcomp(polyorder polyrcf interval polyXY) mathcomp(qe_rcf_th ordered_qelim mxtens)