proposition: Lemma sgp_right_rec p x : sgp_right p x = (if p == 0 then 0 else if ~~ root p x then sgr p.[x] else sgp_right p^`() x).
proof: Proof. rewrite /sgp_right; case hs: size => [|s]; rewrite -size_poly_eq0 hs //=. by rewrite size_deriv hs. 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)