proposition: Lemma jump_mul2r (p q r : {poly R}) : p != 0 -> jump (q * p) (r * p) =1 jump q r.
proof: Proof. by move=> p0 x; rewrite ![_ * p]mulrC jump_mul2l. 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)