proposition: Lemma accr_negN p a r : accr_pos p a r -> accr_neg (- p) a r.
proof: Proof. case=> [[k k_gt0 hk] h]. split; [ exists k=> // x y nxy hx hy; by rewrite !hornerN -opprD mulNr ltr_opp2; apply: hk | by move=> x hx; rewrite derivN hornerN oppr_lt0; apply: h ]. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq choice fintype) mathcomp(bigop order ssralg ssrnum ssrint rat poly polydiv polyorder) mathcomp(perm matrix mxpoly polyXY binomial bigenough)