proposition: Lemma jump_mulCp c p q x : jump (c *: p) q x = (sgz c) * jump p q x.
proof: Proof. have [->|c0] := eqVneq c 0; first by rewrite sgz0 scale0r jump0p mul0r. have [->|p0] := eqVneq p 0; first by rewrite scaler0 jump0p mulr0. have [->|q0] := eqVneq q 0; first by rewrite !jumppc mulr0. rewrite /jump scale_poly_eq0 mu_mulC ?negb_or ?c0 ?p0 ?andTb //. rewrite -scalerAl sgp_right_scale //. case: sgzP c0 => // _ _; rewrite !(mul1r, mulN1r, =^~ mulNrn) //. by rewrite ?oppr_cp0 lt0r sgp_right_eq0 ?mulf_neq0 // andTb leNgt signrN. 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)