proposition: Lemma eval_BoundingPoly e sq : eval_poly e (BoundingPoly sq) = bounding_poly (map (eval_poly e) sq).
proof: Proof. rewrite eval_Deriv -bigop.unlock; congr _^`(); rewrite big_map. by apply: big_morph => [p q | ]/=; rewrite ?eval_MulPoly // mul0r add0r. 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)