proposition: Theorem ComputeBound_nth0 prec pi p X : pi >:: p -> X >: 0 -> forall r : R, (Pol.nth pi 0) >: r -> ComputeBound prec pi X >: r.
proof: Proof. move=> Hpi HX0 r Hr. case E: (Pol.size pi) =>[|n]. have->: r = PolR.horner tt p 0%R. rewrite Pol.nth_default ?E // I.zero_correct /= in Hr. have [A B] := Hr. have H := Rle_antisym _ _ B A. rewrite PolR.hornerE big1 //. by move=> i _; rewrite (Pol.nth_default_alt Hpi) ?E // Rmult_0_l. exact: ComputeBound_correct. have->: r = PolR.horner tt (PolR.set_nth p 0 r) 0%R. rewrite PolR.hornerE PolR.size_set_nth max1n big_nat_recl //. rewrite PolR.nth_set_nth eqxx pow_O Rmult_1_r big1 ?Rplus_0_r //. by move=> i _; rewrite pow_ne_zero ?Rmult_0_r. apply: ComputeBound_correct =>//. have->: pi = Pol.set_nth pi 0 (Pol.nth pi 0). by rewrite Pol.set_nth_nth // E. exact: Pol.set_nth_correct. Qed.
imports: Coq(ZArith Reals Psatz) mathcomp.ssreflect(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype bigop) Interval MathComp Datatypes