fact: Definition jump q p x: int := let non_null := (q != 0) && odd (\mu_x p - \mu_x q) in let sign := (sgp_right (q * p) x < 0)%R in (-1) ^+ sign *+ non_null.
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)