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). set s := (schange_index p). have pa: forall k:nat, k \in s -> p`_k * q`_k < 0. move => k ks. move: (schangei_correct ks) => [eq1 eq2]. have rhsp: 0 < p`_k * (p`_k * x) by rewrite mulrA pmulr_lgt0 // square_pos. rewrite /q mulrBr coefB coefMC mulrBr subr_lt0 coefMX (le_lt_trans _ rhsp)//. by move: eq2; case k. have: schange_index p = s by []. have lcpnz: lead_coef p != 0 by rewrite lead_coef_eq0. have lpp: lead_coef p \in polyseq p by apply: mem_nth; rewrite {2} spp. move: (eq_refl s); rewrite {1}/s; case s. by move /eqP /schangei0 => ap; move:lcpnz; move /(allP ap): lpp => ->. move => i l0 _ sv0. have pb: 0 < p`_(last 0%N s) * q`_(size p). 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. move: (lastI i l0) lcpnz; rewrite - sv0 => sv1. move:(schangei_tail sv1) => [l1 [a [l2 [pv sl1 pn]]]]. have ->: last 0%N s = (last i l0) by rewrite /s sv1 last_rcons. have: lead_coef p = last 0 p by rewrite (last_nth 0) spp. rewrite pv last_cat last_cons; case l2. move => /= ->; move: pn; rewrite pv - cat1s catA mulrC. by rewrite (nth_cat 0 (l1 ++ [:: a])) size_cat addn1 ltnS sl1. by move => b l anz lpv; rewrite (allP lpv) // anz /= mem_last. have rec0: forall l1 l2, l2`_0 != 0 -> (schange (l2) <= schange (l1++l2))%N. by move => l1; case => // a l2 /= anz; rewrite (schange_cat _ _ anz) leq_addl. have ncat: forall l1 l2 b, (l1++l2)`_( (size l1) +b) = l2`_b. by move=> l1 l2 b; rewrite nth_cat addKn -ltn_subRL subnn. move: pa pb;rewrite -{1} schangeE /s sv0 /=. move: sv0 => /schangei_snn [l1 [a [l2 [-> pa pb pc pd]]]] ha hb. have he: (l1 ++ a :: l2)`_i = a by rewrite nth_cat pb ltnn subnn. have skm: forall k, (l1 ++ a :: l2)`_(k + i) = (a::l2)`_k. by move => k; rewrite addnC pb ncat. have hc: a * q`_i < 0 by rewrite -he;apply: ha; rewrite mem_head. have[l2a [l2b [l2v sl]]]: exists l2a l2b, l2a ++ l2b = q /\ size l2a = i. exists (take i q), (drop i q); split; first by exact: cat_take_drop. apply: size_takel; case /orP:(leq_total i (size q)) => //. by move/(nth_default 0) => h; move: hc; rewrite h mulr0 ltxx. move: (hc); rewrite -l2v nth_cat -sl ltnn subnn => hc'. apply: (leq_trans _ (rec0 l2a l2b (proj2 (product_neg hc')))). have sv:[seq (z + i)%N | z <- SIA l2 1 a] = l0 by rewrite pb -pd -schangei_addm. have: forall k, k \in (SIA l2 1 a) -> (a::l2)`_(k-0)%N * l2b`_(k-0%N) < 0. move => k ka; rewrite - skm subn0. have ->: l2b`_k = q`_(k+i) by rewrite -l2v - sl addnC ncat. by apply: ha;rewrite inE - sv (mem_map (@addIn i)) ka orbT. have: 0 < (a :: l2)`_((last 0%N (SIA l2 1 a)) -0) * l2b`_(size l2).+1. move: hb; rewrite -sv /= (last_map (fun z=> (z + i)%N) (SIA l2 1 a) 0%N). by rewrite subn0 skm - l2v size_cat -pb - sl ncat. rewrite - sv size_map. move: rec0 ncat hc' pa; clear; move => rec0 ncat hc' pa. move: {2 3 4 5} (SIA l2 1 a) pa (erefl (SIA l2 1 a)) hc'. rewrite - (addn0 1%N); move: {2 4 5 6 7} 0%N. move => n s; move: s a n l2 l2b; elim. move => a n l l' _ anz pnz;set j := (size l).+1 %N. rewrite /last subnn {1}/nth mulrC ; move => lt2 _. move:(prodNsimpl_gt pnz lt2);apply: schange_nz. move => i s Hrec a n l l' anz. move /(schangei_recc anz)=> [l1 [b [l2 [-> pa pb pc [pd pe]]]]]. move => qa qb qc /=. have imn: (i - n = (size l1).+1) %N by rewrite pd addnAC add1n addnK. have: (i\in i :: s) by rewrite mem_head. move /qc; rewrite imn -cat1s catA nth_cat subnn ltnn - imn => e1. set ni := (i - n )%N. move: (cat_take_drop ni l'). set l1' := take ni l'; set l2' := drop ni l' => e2. have e3: size l1' = ni. move: e1;rewrite size_take; case (leqP (size l') ni) => //. by move/(nth_default 0) => ->; rewrite mulr0 ltxx. move: (prodNsimpl_lt qa pa); rewrite mulrC => e4. move: (prodNsimpl_gt e1 e4) => e5. move: (proj2 (product_neg e5)); set w := l'`_ni => wnz. have [u l2v]: exists u, l2' = w::u. move: wnz;rewrite /w - e2 nth_cat e3 ltnn subnn. case l2'; [ by rewrite eqxx | by move => a1 b1 _; exists b1]. move: (schange_cat l1' u wnz); rewrite - l2v e2 => ->. suff: ((size s) < schange l2')%N. set l1'' := (l1' ++ [:: w]). have : l1''`_0 * l1''`_ni < 0. move: e5; rewrite -e2 l2v /l1'' !nth_cat e3 ltnn subnn; case i => //. by move/schange_nz => e6 e7; move: (leq_add e6 e7); rewrite add1n. clear u l2v. have r0: b * l2'`_0 < 0 by move: e1; rewrite - e2 nth_cat e3 ltnn subnn. move: pe; rewrite -pd - add1n => r1. have r2 : (forall k, k \in s -> (b :: l2)`_(k - i) * l2'`_(k - i) < 0). move => k ks; have: k \in i::s by rewrite inE ks orbT. move: ks; rewrite -{1} r1 schangei_addm; move /mapP => [k' k'v kv]. have ->: (k - i)%N = k' by rewrite kv addnK. move/ qc; rewrite - e2 - cat1s catA. have ->: (k - n = k' + (size l1).+1)%N. by rewrite kv pd addnAC add1n addnA addnK. by rewrite addnC ncat -imn -/ni -e3 ncat. have r3: 0 < (b :: l2)`_(last i s - i) * l2'`_(size l2).+1. move:qb; rewrite - e2 size_cat - addSn - imn -/ni -e3 ncat. suff: ((last n (i :: s) - n) = ni + (last i s - i)) %N. by move => ->; rewrite /ni imn - cat1s catA ncat. have lni: (n<=i) %N by rewrite pd addnAC leq_addl. rewrite -r1 schangei_addm; case (SIA l2 1 b); first by rewrite /= subnn addn0. move => n0 l0 /=; set la := last _ _. have eq1: (i <= la)%N. by rewrite /la (last_map (fun z=> (z + i)%N)) leq_addl. by rewrite - {1} (subnK eq1) - (addnBA _ lni) addnC. exact: (Hrec b i l2 l2' pb r1 r0 r3 r2). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice fintype order) mathcomp(binomial bigop ssralg poly ssrnum ssrint rat) mathcomp(polydiv polyorder path interval polyrcf)