proposition: Lemma npos_roots0 p: (p != 0 /\ p^`() != 0) \/ (npos_roots p = 0)%N.
proof: Proof. case (eqVneq p 0) => pnz. right; rewrite /npos_roots /pos_roots. move: (poly_split_fact p) => H; move: (s2valP' H) (s2valP H) => [_ h1] _. by rewrite (proj1 (h1 pnz)) // big_nil. move: (pos_split1 pnz) => [[pa pb pc pd] pe pf]. case (leqP (size p) 1%N) => sp; [right | left]. move: pf sp; rewrite (pos_split_deg pnz) - size_poly_gt0. case: (size (pos_cofactor p)) => //. by move => m _; rewrite addnS ltnS leqn0 addn_eq0 => /andP [/eqP -> _]. split => //. by rewrite -size_poly_eq0 (size_deriv p); move: sp;case: (size p)=> //; case. 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)