proposition: Lemma schange_parity p: p != 0 -> odd (npos_roots p) = odd (schange p).
proof: Proof. move => pnz. move: (npos_root_parity pnz) (schange_odd pnz). case h: (0 < lead_tail_coef p)%R; last by rewrite !addn0 => ->. by rewrite ! addn1 /= => /negbTE -> /negbTE ->. 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)