proposition: Lemma sgp_rightNroot (p : {poly R}) x : ~~ root p x -> sgp_right p x = sgr p.[x].
proof: Proof. move=> nrpx; rewrite /sgp_right; case hsp: (size _)=> [|sp]. by move/eqP:hsp; rewrite size_poly_eq0; move/eqP->; rewrite hornerC sgr0. by rewrite nrpx. 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)