proposition: Lemma eval_AddPoly p q e : eval_poly e (p ++ q)%qfT = (eval_poly e p) + (eval_poly e q).
proof: Proof. elim: p q => [|a p Hp] q /=; first by rewrite add0r. case: q => [|b q] /=; first by rewrite addr0. by rewrite Hp mulrDl rmorphD /= !addrA [X in _ = X + _]addrAC. 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)