proposition: Lemma mu_mod p q x : (\mu_x p < \mu_x q)%N -> \mu_x (rmodp p q) = \mu_x p.
proof: Proof. move=> mupq; have [->|p0] := eqVneq p 0; first by rewrite rmod0p. have qn0 : q != 0 by apply: contraTneq mupq => ->; rewrite mu0 ltn0. have /(canLR (addKr _)) <- := (rdivp_eq q p). have [->|divpq_eq0] := eqVneq (rdivp p q) 0. by rewrite mul0r oppr0 add0r mu_mulC ?lcn_neq0. rewrite mu_addl ?mu_mulC ?scaler_eq0 ?negb_or ?mulf_neq0 ?lcn_neq0 //. by rewrite mu_opp mu_mul ?ltn_addl // ?mulf_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)