proposition: Lemma descartes p: p != 0 -> (odd (npos_roots p) = odd (schange p) /\ ((npos_roots p) <= (schange p)) %N).
proof: Proof. move => pa; split; first by apply:schange_parity. move: (pos_split1 pa); rewrite /npos_roots; move => [[p1 p2 p3 p4] p5 qnz]. have [s [sa <- <-]]: exists s, [/\ (all [eta <%R 0] s), size s = (\sum_(i <- pos_roots p) i.2)%N & \prod_(z <- s) ('X - z%:P) * pos_cofactor p = p]. rewrite {3}p1;move: p2;elim: (pos_roots p) => [_ | a l Hrec /= /andP [q1 q2]]. by exists [::]; rewrite ! big_nil. move: (Hrec q2) => [s [s1 s2 s3]]; exists ((nseq a.2 a.1) ++ s). rewrite all_cat s1 ! big_cons -s2 size_cat size_nseq andbT; split => //. have: all (pred1 a.1) (nseq a.2 a.1). by rewrite all_pred1_nseq. by move => h; apply /allP => x; move /(allP h) => /= /eqP ->//. rewrite big_cat /= - ! mulrA -s3 ;congr ( _ * _). rewrite (big_nth 0) big_mkord (eq_bigr (fun _ => ('X - a.1%:P)))=>[|[i]] /=. by rewrite prodr_const card_ord size_nseq. by rewrite size_nseq nth_nseq=> ->. move: (pos_cofactor p) sa qnz ;clear; elim s; first by move => p _ pnz //. move => a l Hrec p /= /andP [ap alp] pnz. rewrite big_cons - mulrA mulrC; move: (Hrec _ alp pnz); set q := _ * _ => e1. have qnz: q !=0 by rewrite mulf_neq0 //; apply: monic_neq0; apply: monic_prod_XsubC. exact (leq_ltn_trans e1 (pol_mul_cs qnz ap)). 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)