fact: Definition sjump p x : int := ((-1) ^+ (sgp_right p x < 0)%R) *+ odd (\mu_x p).
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq choice path fintype) mathcomp(div bigop order ssralg poly polydiv ssrnum perm zmodp ssrint) mathcomp(polyorder polyrcf interval matrix mxtens)