proposition: Lemma descartes_bis 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: p {2}(size p) (leqnn (size p)) pa => p n; move:p; elim:n. by move => p;rewrite size_poly_leq0 => ->. move => n Hrec p spn pnz. move: (schange_parity pnz) => od. case (npos_roots0 p); [move => [_ dnz] | by move => ->]. move: (leq_trans (lt_size_deriv pnz) spn); rewrite ltnS=> spln. move:(Hrec _ spln dnz); rewrite - ltnS => /(leq_trans (pos_root_deriv p)) eq3. move: od; case (schange_deriv p); move => -> //; move: eq3;set s := schange _. by rewrite leq_eqVlt ltnS;case /orP => // /eqP -> /=;case (odd _). 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)