proposition: Lemma pol_approx_prop (p : {poly R}) (a b: R) n: p.[a] < 0 -> 0 <= p.[b] -> a < b -> let:(u,v) := (pol_approx p (a,b) n) in [&& (v-u) == (b-a) / (2%:R ^+ n), pair_in_interval a u v b, p.[u] < 0 & 0 <= p.[v] ].
proof: Proof. move => pan pbp lab. elim:n;first by rewrite /= expr0 divr1 eqxx /pair_in_interval pan pbp lab !lexx. move => n /=; case (pol_approx p (a,b) n) => u v /and4P [/eqP d1 pi pun pvp]. have aux: half ((b - a) / 2%:R ^+ n) == (b - a) / 2%:R ^+ n.+1. by rewrite /half exprS -mulrA - invrM // ? unitrX ? two_unit. rewrite /pol_next_approx /pair_in_interval;case /and3P: pi => [au uv vb]. case cp:(p.[u] * p.[half (u + v)] <= 0). case /andP: (mid_between uv) => [h1 h2]. rewrite -{2}(double_half u) half_lin half_lin1 opprD. rewrite addrA {1} (addrC u) addrK d1 aux pun - (nmulr_rle0 _ pun) cp. by rewrite au h1 (ltW (lt_le_trans h2 vb)). case /andP: (mid_between uv) => [h1 h2]. rewrite -{1}(double_half v) half_lin half_lin1 opprD - addrA (addrA _ (-u)). rewrite (addrC _ (-u)) addrK d1 aux pvp h2 vb (ltW (le_lt_trans au h1)). by rewrite -(nmulr_rgt0 _ pun) ltNge cp. Qed.
imports: mathcomp(all_ssreflect) mathcomp(ssralg poly ssrnum ssrint rat polyrcf) mathcomp(polyorder polydiv)