proposition: Lemma sjump_neigh a b p x : p != 0 -> {in neighpl p a x & neighpr p x b, forall yl yr, sjump p x = cross p yl yr}.
proof: Proof. move=> pn0 yl yr yln yrn; rewrite /cross /variation. rewrite -sgr_cp0 sgrM /sjump (sgr_neighpl yln) -!(sgr_neighpr yrn). rewrite -mulrA -expr2 sqr_sg (rootPf (neighpr_root yrn)) mulr1. rewrite sgrEz ltrz0 -[in rhs in _ = rhs]intr_sign -[X in _ == X]mulrN1z eqr_int. by have /rootPf := neighpr_root yrn; case: sgzP; case: odd. 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)