proposition: Lemma bounding_polyP (sq : seq {poly R}) : [\/ \big[andb/true]_(q <- sq) (lead_coef q > 0), \big[andb/true]_(q <- sq) ((-1)^+(size q).-1 * (lead_coef q) > 0) | exists x, ((bounding_poly sq).[x] == 0) && \big[andb/true]_(q <- sq) (q.[x] > 0)] <-> exists x, \big[andb/true]_(q <- sq) (q.[x] > 0).
proof: Proof. split=> [|[x]]. case; last by move=> [x /andP [? h]]; exists x; rewrite h. rewrite big_all => /allP hsq. have sqn0 : {in sq, forall q, q != 0}. by move=> q' /= /hsq; apply: contraL=> /eqP->; rewrite lead_coef0 ltxx. pose qq := \prod_(q <- sq) q. have pn0 : qq != 0. by apply/negP=> /myprodf_eq0 [] q; rewrite andbT => /sqn0 /negPf ->. pose b := cauchy_bound qq; exists b. rewrite big_all; apply/allP=> r hr; have:= hsq r hr. rewrite -!sgr_cp0=> /eqP <-; apply/eqP. apply: (@sgp_pinftyP _ b); last by rewrite boundl_in_itv. move=> z Hz /=; have: ~~ root qq z by rewrite ge_cauchy_bound. by rewrite /root /qq horner_prod prodf_seq_neq0 => /allP /(_ _ hr). rewrite big_all => /allP hsq. have sqn0 : {in sq, forall q, q != 0}. move=> q' /= /hsq; apply: contraL=> /eqP->. by rewrite lead_coef0 mulr0 ltxx. pose qq := \prod_(q <- sq) q. have pn0 : qq != 0. by apply/negP=> /myprodf_eq0 [] q; rewrite andbT => /sqn0 /negPf ->. pose b := - cauchy_bound qq; exists b. rewrite big_all; apply/allP=> r hr; have:= hsq r hr. rewrite -!sgr_cp0=> /eqP <-; apply/eqP. apply: (@sgp_minftyP _ b); last by rewrite boundr_in_itv. move=> z Hz /=; have: ~~ root qq z by rewrite le_cauchy_bound. by rewrite /root /qq horner_prod prodf_seq_neq0 => /allP /(_ _ hr). rewrite /bounding_poly; set q := \prod_(q <- _) _. rewrite big_all => /allP hsq; set bnd := cauchy_bound q. have sqn0 : {in sq, forall q, q != 0}. by move=> q' /= /hsq; apply: contraL=> /eqP->; rewrite horner0 ltxx. have [/eqP|q_neq0] := eqVneq q 0. by rewrite prodf_seq_eq0=> /hasP [q' /= /sqn0 /negPf->]. have genroot y : {in sq, forall r, ~~ root q y -> ~~ root r y}. rewrite /root /q => r r_sq. by rewrite horner_prod prodf_seq_neq0 => /allP /(_ _ r_sq). case: (next_rootP q x bnd) q_neq0; [by move->; rewrite eqxx| |]; last first. move=> _ q_neq0 _ Hq _. suff -> : \big[andb/true]_(q1 <- sq) (0 < lead_coef q1) by constructor. rewrite big_all; apply/allP=> r hr; have rxp := hsq r hr. rewrite -sgr_cp0 -/(sgp_pinfty _). rewrite -(@sgp_pinftyP _ x _ _ x) ?boundl_in_itv ?sgr_cp0 //. move=> z; rewrite (@itv_splitU _ _ (BRight x)) /<=%O /= ?lexx //. rewrite itv_xx /= => /orP [/eqP->|]; first by rewrite /root gt_eqF. have [x_b|b_x] := ltrP x bnd. rewrite (@itv_splitU _ _ (BLeft bnd)) /<=%O /= ?x_b //. move=> /orP [] Hz; rewrite genroot //; by [rewrite Hq|rewrite ge_cauchy_bound]. move=> Hz. by rewrite genroot ?ge_cauchy_bound // (subitvP _ Hz) /<=%O /= /<=%O //= b_x. move=> y1 _ rqy1 hy1xb hy1. case: (prev_rootP q (- bnd) x); [by move->; rewrite eqxx| |]; last first. move=> _ q_neq0 _ Hq _. suff -> : \big[andb/true]_(q1 <- sq) (0 < (-1) ^+ (size q1).-1 * lead_coef q1). by constructor 2. rewrite big_all; apply/allP=> r hr; have rxp := hsq r hr. rewrite -sgr_cp0 -/(sgp_minfty _). rewrite -(@sgp_minftyP _ x _ _ x) ?boundr_in_itv ?sgr_cp0 //. move=> z; rewrite (@itv_splitU _ _ (BLeft x)) /<=%O /= ?lexx //. rewrite itv_xx => /orP [/=|/eqP->]; last by rewrite /root gt_eqF. have [b_x|x_b] := ltrP (- bnd) x. rewrite (@itv_splitU _ _ (BRight (- bnd))) /<=%O /= ?b_x //. move=> /orP [] Hz; rewrite genroot //; by [rewrite Hq|rewrite le_cauchy_bound]. by move=> Hz; rewrite genroot // le_cauchy_bound // (subitvP _ Hz) //= x_b. move=> y2 _ rqy2 hy2xb hy2 q_neq0. have lty12 : y2 < y1. by apply: lt_trans (_ : x < _); rewrite 1?(itvP hy1xb) 1?(itvP hy2xb). have : q.[y2] = q.[y1] by rewrite rqy1 rqy2. case/(rolle lty12) => z hz rz; constructor 3; exists z. rewrite rz eqxx /= big_all; apply/allP => r r_sq. have xy : x \in `]y2, y1[ by rewrite in_itv /= 1?(itvP hy1xb) 1?(itvP hy2xb). rewrite -sgr_cp0 (@polyrN0_itv _ `]y2, y1[ _ _ x) ?sgr_cp0 ?hsq // => t. rewrite (@itv_splitUeq _ _ x) // => /or3P [/hy2|/eqP->|/hy1]; do ?exact: genroot. by rewrite rootE gt_eqF ?hsq. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq choice path fintype) mathcomp(div bigop order ssralg poly polydiv ssrnum perm zmodp ssrint) mathcomp(polyorder polyrcf interval matrix mxtens)