proposition: Lemma pol_mul_cs (p: {poly R}) (x: R): p !=0 -> x > 0 -> ( (schange p) < (schange (p * ('X - x%:P))%R))%N.
proof: Proof. move => pnz xn. set q := _ * _. have spp: size p = (size p).-1.+1. by move: pnz; rewrite -size_poly_eq0; case sz:(size p). have lcpnz: lead_coef p != 0 by rewrite lead_coef_eq0. set s := (schange_index p). suff: (forall k, k \in s -> p`_k * q`_k < 0) /\ 0 < p`_(last 0%N s) * q`_(size p). by move => [pa pb];apply: schange_monotone. have -> : q`_(size p) = lead_coef p. move: (monicXsubC x) => mc; rewrite- (lead_coef_Mmonic p mc) lead_coefE. by rewrite (size_Mmonic pnz mc) size_XsubC addn2. have lpp: lead_coef p \in polyseq p by apply: mem_nth; rewrite {2} spp. have [heads [lasts sv]]: exists a b, s = rcons a b. move: (eq_refl s); rewrite {1}/s; case s. by move /eqP /schangei0 => ap; move:lcpnz; move /(allP ap): lpp => ->. by move => n l _; rewrite lastI; exists (belast n l), (last n l). move:(schange_index_tail sv) => [l1 [a [l2 [pv sl1 pn alz]]]]. have ->: last 0%N s = lasts by rewrite sv last_rcons. have: lead_coef p = last 0 p by rewrite (last_nth 0) spp. rewrite {1 3} pv last_cat last_cons; move: alz. case l2; last first. move => b l az /= lpv; move: lcpnz. have: lead_coef p \in (b :: l) by rewrite lpv mem_last. by move /(allP az) => ->. move => _ /= ->; split; last first. move: pn; rewrite pv - cat1s catA mulrC (nth_cat 0 (l1 ++ [:: a])). by rewrite size_cat addn1 ltnS sl1. clear heads lasts sl1 a l2 pv sl1 pn sv. move => k ks. move: (schange_index_correct ks) => [eq1 eq2]. have rhsp: 0 < p`_k * (p`_k * x). by rewrite mulrA (pmulr_lgt0 _ xn) lt0r sqr_ge0 sqrf_eq0 eq1. rewrite /q mulrBr coefB coefMC mulrBr subr_lt0 coefMX (le_lt_trans _ rhsp) //. by move: eq2; case k. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice fintype order) mathcomp(binomial bigop ssralg poly ssrnum ssrint rat) mathcomp(polyrcf) pol