proposition: Lemma npos_root_parity p: p != 0 -> odd (npos_roots p + (0< lead_tail_coef p)%R).
proof: Proof. move => pnz; move: (pos_split1 pnz) => [[pv pb pc] pd qp qnz]. rewrite {2} pv;set r := \prod_(z <- _) _. have rm: r \is monic by apply:monic_prod_XsubCe. rewrite lead_tail_coefM (pmulr_lgt0 _ (noproots_cs qp)) /lead_tail_coef. move: (refl_equal (sgr r`_0)); rewrite - {2} horner_coef0 horner_prod. set X := \prod_(z <- _) _; have ->: X = \prod_(i <- pos_roots p) (- i.1)^+ i.2. by apply: eq_big => // i _; rewrite horner_exp hornerXsubC sub0r. have ->: Num.sg (\prod_(i <- pos_roots p) (- i.1) ^+ i.2) = (-1) ^+ \sum_(i <- pos_roots p) (i.2). move: pb; elim (pos_roots p) => [ _ | i rr /= Hr /andP [pa pb]]. by rewrite !big_nil sgr1. by rewrite !big_cons sgrM sgrX Hr // sgrN (gtr0_sg pa) exprD. move => aux. case (eqVneq r`_0 0) => nr0. by move: aux; rewrite nr0 sgr0 => /eqP; rewrite eq_sym signr_eq0. rewrite (eqP rm) mulr1 (tail_coef0b nr0) -sgr_gt0 aux - signr_odd signr_gt0. by case h: (odd(npos_roots p)); [ rewrite addn0 | rewrite addn1 /= h]. 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)