proposition: Lemma jump_neigh a b p q x : q * p != 0 -> {in neighpl (q * p) a x & neighpr (q * p) x b, forall yl yr, jump q p x = cross (q * p) yl yr *+ ((q != 0) && (\mu_x p > \mu_x q)%N)}.
proof: Proof. move=> pqn0 yl yr hyl hyr; rewrite -(sjump_neigh pqn0 hyl hyr). rewrite /jump /sjump -mulrnA mulnb andbCA. have [muqp|/eqnP ->] := ltnP; rewrite (andbF, andbT) //. by rewrite mu_mul // oddD addbC oddB // ltnW. 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)