proposition: Lemma jump_mod p q x : jump p q x = sgz (lead_coef q) ^+ (rscalp p q) * jump (rmodp p q) q x.
proof: Proof. case p0: (p == 0); first by rewrite (eqP p0) rmod0p jump0p mulr0. case q0: (q == 0); first by rewrite (eqP q0) rmodp0 jumppc mulr0. rewrite -sgzX; set s := sgz _. apply: (@mulfI _ s); first by rewrite /s sgz_eq0 lcn_neq0. rewrite mulrA mulz_sg lcn_neq0 mul1r -jump_mulCp rdivp_eq. have [->|rpq_eq0] := altP (rmodp p q =P 0). by rewrite addr0 jump0p -[X in jump _ X]mul1r jump_mul2r ?q0 // jumppc. rewrite /jump. set r := _ * q + _. have muxp : \mu_x p = \mu_x r by rewrite /r -rdivp_eq mu_mulC ?lcn_neq0. have r_neq0 : r != 0 by rewrite /r -rdivp_eq scaler_eq0 p0 orbF lcn_neq0. have [hpq|hpq] := leqP (\mu_x q) (\mu_x r). rewrite 2!(_ : _ - _ = 0)%N ?andbF //; apply/eqP; rewrite -/(_ <= _)%N //. by rewrite mu_mod_leq ?dvdpE // muxp. rewrite mu_mod ?muxp // rpq_eq0 (negPf r_neq0); congr (_ ^+ _ *+ _). rewrite !sgp_right_mul sgp_right_mod ?muxp // /r -rdivp_eq. by rewrite -mul_polyC sgp_right_mul sgp_rightc sgrX. 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)