proposition: Lemma schange_monotone l l' (s:= schange_index l): (forall k, k \in s ->l`_k * l'`_k <0) -> l`_ (last 0%N s) * l'`_(size l) > 0 -> (schange l < schange l') %N.
proof: Proof. have: schange_index l = s by []. case: s. move/schangei0 => alz _; rewrite /last. suff: l`_0 = 0 by move => ->; rewrite mul0r ltxx. by move: alz; case l => // a l1 /= /andP [/eqP ->]. 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 rec1: forall l i j, l`_i * l`_j < 0 -> (0 < (schange l))%N. move => l1 i j; wlog : i j / (i<= j)%N. by case /orP:(leq_total i j)=> cij h; [ | rewrite mulrC]; apply:h. move => lij ov. move: (product_neg ov) => [anz bnz]. have st: size (take i l1) = i. rewrite size_take; case (ltnP i (size l1)) => // sl. by move: anz; rewrite (nth_default 0 sl) eqxx. move: (cat_take_drop i l1) => eq1. have e2: l1`_i = (drop i l1)`_0 by rewrite - {1} eq1 nth_cat st ltnn subnn. have e3: (drop i l1)`_0 != 0 by rewrite - e2. have e4: l1`_j = (drop i l1)`_(j-i) by rewrite -{1}eq1 nth_cat st ltnNge lij. move:ov; rewrite e2 e4; set l3 := (drop i l1); set k:= (j - i)%N => ov. move: (rec0 (take i l1) l3 e3); rewrite eq1; apply: leq_trans. have st': size (take k l3) = k. rewrite size_take; case (ltnP k (size l3)) => // sl. by move: bnz; rewrite e4 (nth_default 0 sl) eqxx. move: (cat_take_drop k l3) => eq2. have l3k: l3`_k = (drop k l3)`_0 by rewrite - {1} eq2 nth_cat st' ltnn subnn. have l3knz: l3`_k != 0 by rewrite /l3 /k - e4. have [v eq6]: exists v, (drop k l3) = l3`_k:: v. move:l3knz; rewrite l3k ;case (drop k l3); last by move => a b _; exists b. by rewrite eqxx. have [u eq7]: exists u, (take k l3) = l3`_0:: u. move: st'; rewrite -{3} eq2; case (take k l3). by move => /= kz; move: ov; rewrite -kz ltNge sqr_ge0. by move => a b _; exists b. rewrite -eq2 eq6 schange_cat // eq7 cat_cons. by move: (schange_odd1 u ov); set w :=schange _; case w. 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 => i s sil ha hb. rewrite {1} /schange sil /=; move: sil ha hb. move /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 * l'`_i < 0 by rewrite -he;apply: ha; rewrite mem_head. have[l2a [l2b [l2v sl]]]: exists l2a l2b, l2a ++ l2b = l' /\ size l2a = i. exists (take i l'), (drop i l'); split; first by exact: cat_take_drop. apply: size_takel; case /orP:(leq_total i (size l')) => //. 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] = s 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 = l'`_(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. clear he sv skm pb pc pd ha sl s hb l2v hc l2a he l1 l l' i. 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:(schange_simpl1 pnz lt2);apply: rec1. 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: (schange_simpl2 qa pa); rewrite mulrC => e4. move: (schange_simpl1 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/rec1 => 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(polyrcf) pol