proposition: Lemma sgp_right_deriv (p : {poly R}) x : root p x -> sgp_right p x = sgp_right (p^`()) x.
proof: Proof. elim: (size p) {-2}p (erefl (size p)) x => {p} [p|sp hp p hsp x]. by move/eqP; rewrite size_poly_eq0; move/eqP=> -> x _; rewrite derivC. by rewrite /sgp_right size_deriv hsp /= => ->. 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)