proposition: Lemma schangeE l: (size (schange_index l)).-1 = (schange l).
proof: Proof. transitivity ((size (schange_index (filter (fun z => z != 0) l))).-1). have aux: forall l, (all_eq0 l) -> filter (fun z => z != 0) l = [::]. by elim => // a l' Hr /= /andP [-> /Hr ->]. rewrite /schange; case alz: (all_eq0 l). by rewrite (aux _ alz) - {1} (cats0 l) schangei_s0. move: (negbT alz); rewrite - (has_predC) => /has_split_eq. move => [l1 [b [l2 [-> pb pc]]]]; rewrite filter_cat aux //= pb. rewrite schangei_s0 // /schange_index /= eqxx pb /=. move: b (size l1).+1 1%N pb; elim: l2 => // a l' Hrec b n m bnz /=. case (eqVneq a 0). by move => ->; rewrite mul0r eqxx ltxx andbF /=; apply: Hrec. move =>h; rewrite h /= (negbTE bnz) /=. by case h':(a * b < 0); [ simpl; congr S |]; apply: Hrec. move: (filter_all (fun z => z != 0) l); rewrite -/(filter0 l). rewrite /schange; case (filter0 l) => // a s /= /andP [anz ar]. rewrite /schange_index /SIA -/SIA eqxx anz andbT orTb /=. move: 1%N a anz ar; elim:s; first by move => a n _ _ /=; rewrite mulr0 ltxx. move => a s Hrec n b bnz /= /andP [anz ar]; rewrite mulrC anz (negbTE bnz) /=. case h:(b * a < 0) => /=; rewrite Hrec // add0n. have: (0 < b * a) by rewrite lt0r mulf_neq0 // leNgt h. case (ltrgt0P a) => ap //; last by move: anz; rewrite ap eqxx. by rewrite (pmulr_lgt0) // => bp; rewrite ! (pmulr_rlt0). by rewrite (nmulr_lgt0) // => bp; rewrite ! (nmulr_rlt0). 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)