proposition: Lemma ders0l : p.[b] = 0 -> {in `[a, b[, forall x, sgr p.[x] = -sp'c}.
proof: Proof. move=> pb0 x hx; rewrite hsgpN // (lt_le_trans (derq0l _)) //. by rewrite hornerZ pb0 mulr0. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq choice fintype) mathcomp(bigop order ssralg poly polydiv ssrnum zmodp) mathcomp(polyorder path interval ssrint)