proposition: Lemma noroot_jump q p x : ~~ root p x -> jump q p x = 0.
proof: Proof. have [->|p_neq0] := eqVneq p 0; first by rewrite jumppc. by rewrite -mu_gt0 // lt0n negbK /jump => /eqP ->; rewrite andbF mulr0n. Qed.
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)