proposition: Lemma mu_mod_leq : forall p q x, ~~ (q %| p) -> (\mu_x q <= \mu_x p)%N -> (\mu_x q <= \mu_x (rmodp p q)%R)%N.
proof: Proof. move=> p q x; rewrite dvdpE /rdvdp=> rn0 mupq. case q0: (q == 0); first by rewrite (eqP q0) mu0 leq0n. move/eqP: (rdivp_eq q p). rewrite eq_sym (can2_eq (addKr _ ) (addNKr _)); move/eqP=> hr. rewrite hr; case qpq0: (rdivp p q == 0). by rewrite (eqP qpq0) mul0r oppr0 add0r mu_mulC // lcn_neq0. rewrite (leq_trans _ (mu_add _ _)) // -?hr //. rewrite leq_min mu_opp mu_mul ?mulf_neq0 ?qpq0 ?q0 // leq_addl. by rewrite mu_mulC // lcn_neq0. 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)