proposition: Lemma jump_mul2l (p q r : {poly R}) : p != 0 -> jump (p * q) (p * r) =1 jump q r.
proof: Proof. move=> p0 x; rewrite /jump. case q0: (q == 0); first by rewrite (eqP q0) mulr0 eqxx. have ->: p * q != 0 by rewrite mulf_neq0 ?p0 ?q0. case r0: (r == 0); first by rewrite (eqP r0) !mulr0 mu0 !sub0n. rewrite !mu_mul ?mulf_neq0 ?andbT ?q0 ?r0 //; rewrite subnDl. rewrite mulrAC mulrA -mulrA. rewrite (@sgp_right_mul _ (p * p)) // sgp_right_mul // sgp_right_square //. by rewrite mul1r mulrC /=. 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)