proposition: Lemma schange_nz l i j: l`_i * l`_j < 0 -> (0 < (schange l))%N.
proof: Proof. move=> pn; move: (product_neg pn) => [xnz ynz]. have aux: forall k, l`_k !=0 -> l`_k \in (filter0 l). move => k kz; rewrite mem_filter kz /= mem_nth //. by case (leqP (size l) k) => h //; move: kz;rewrite nth_default // eqxx. move: pn (aux _ xnz) (aux _ ynz); set x := l`_i; set y := l`_j. move: (filter_all (fun z => z!=0) l); rewrite /schange -/(filter0 l). case (filter0 l) => //. move => a l2 pa pb pc pd. wlog : x y pb pc pd / a * x < 0. move => H; case (ltrgt0P (a * x)) => h; try apply: (H x y pb pc pd h). apply: (H y x) => //; [by rewrite mulrC | exact: (prodNsimpl_gt pb h)]. move: pa => /= /andP [anz _]. by move /eqP: h; rewrite mulf_eq0 (negbTE anz) (negbTE xnz). move: pc; rewrite inE; case /orP. by move /eqP <- => h; move: (lt_trans pb (prodNsimpl_lt pb h)); rewrite ltxx. move: pa; clear; move:a x; elim l2 => //. move => a l H b x /= /andP [bnz bl] ca bcn. case (ltrgt0P (b * a)); last first. by move /eqP; rewrite mulf_eq0 (negbTE bnz)=> /= ane; move: bl; rewrite ane. move=> ->. by rewrite add1n ltnS. rewrite mulrC; move => ba; move: (prodNsimpl_gt bcn ba) => aca. rewrite (ltNge (a * b)) (ltW ba) add0n. apply: (H a x bl) => //; move: ca; rewrite inE; case /orP => // /eqP xa. by move: (lt_trans bcn ba); rewrite xa mulrC ltxx. 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)