proposition: Lemma sgp_right_eq0 (x : R) p : (sgp_right p x == 0) = (p == 0).
proof: Proof. have [->|p0] := eqVneq p; first by rewrite sgp_rightc sgr0 eqxx. rewrite /sgp_right. elim: (size p) {-2}p (erefl (size p)) p0=> {p} [|sp ihsp] p esp p0. by move/eqP: esp; rewrite size_poly_eq0 (negPf p0). rewrite esp /=; case px0: root=> //=; rewrite ?sgr_cp0 ?px0//. have hsp: sp = size p^`() by rewrite size_deriv esp. rewrite hsp ihsp // -size_poly_eq0 -hsp. move: px0; rewrite root_factor_theorem => /rdvdp_leq /(_ p0). by rewrite size_XsubC esp ltnS; case: posnP. 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)