proposition: Lemma schange_odd1 x l y: x * y < 0 -> odd (schange (x::l ++ [::y])).
proof: Proof. move => xy; rewrite /schange. move: (product_neg xy) => [xnz ynz]. set s := schange_index (x :: l ++ [:: y]). move: (refl_equal s); rewrite {1} /s; case: s. have xl: x \in x :: l ++ [:: y] by rewrite mem_head. by move /schangei0 => h; move: xnz; move/(allP h):xl => /eqP ->; rewrite eqxx. move => i s /=. rewrite /schange_index /= eqxx xnz orTb => /eqP; rewrite eqseq_cons => /andP. move => [ _] /eqP. have ->: (size s)= (((x * y>=0)%R) + size s)%N by rewrite leNgt xy. clear i xy;move: x xnz 1%N l; elim: s. move => x xnz n l => /eqP; rewrite -(schangei_reca _ _ xnz) => ss. have: y \in (l ++ [:: y]) by rewrite mem_cat inE eqxx orbT. by move /(allP ss); rewrite mulrC => ->. move => a s Hrec x xnz n l. move/(schangei_recc xnz)=> [l1 [c [l2 [lv pa cnz pb [pc]]]]]. have cp:0 < c * c by rewrite lt0r sqr_ge0 sqrf_eq0 (proj1 (product_neg pa)). have ->: (0 <= x * y) = ~~(0 <= c * y). rewrite - (nmulr_rle0 (c * y) pa) mulrACA (pmulr_rle0 _ cp). by rewrite - ltNge lt_neqAle eq_sym (mulf_neq0 xnz ynz). move: (f_equal (last c) lv); rewrite !last_cat !last_cons /= addnS. case l2; first by move => ->; rewrite (ltW cp) /= => <-. move => i1 l4; rewrite last_cons (lastI i1 l4) - cats1 => <-. move /(Hrec c cnz (n + size l1).+1 _). by case b:((0 <= c * y)%R) => //= ->. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice fintype order) mathcomp(binomial bigop ssralg poly ssrnum ssrint rat) mathcomp(polyrcf) pol