proposition: Lemma jump_coprime p q : p != 0 -> coprimep p q -> forall x, root p x -> jump q p x = sjump (q * p) x.
proof: Proof. move=> pn0 cpq x rpx; rewrite /jump /sjump. have q_neq0 : q != 0; last rewrite q_neq0 /=. apply: contraTneq cpq => ->; rewrite coprimep0. by apply: contraL rpx => /eqp_root ->; rewrite rootC oner_eq0. have := coprimep_root cpq rpx; rewrite -rootE -mu_eq0 => // /eqP muxq_eq0. by rewrite mu_mul ?mulf_neq0 ?muxq_eq0 ?subn0 ?add0n. 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)