proposition: Lemma divzMpl p m d : p > 0 -> (p * m %/ (p * d) = m %/ d)%Z.
proof: Proof. case: p => // p p_gt0; wlog d_gt0: d / d > 0; last case: d => // d in d_gt0 *. by move=> IH; case/intP: d => [|d|d]; rewrite ?mulr0 ?divz0 ?mulrN ?divzN ?IH. rewrite {1}(divz_eq m d) mulrDr mulrCA divzMDl ?mulf_neq0 ?Order.POrderTheory.gt_eqF // addrC. rewrite divz_small ?add0r // PoszM pmulr_rge0 ?modz_ge0 ?Order.POrderTheory.gt_eqF //=. by rewrite ltr_pM2l ?ltz_pmod. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq choice fintype order bigop ssralg) mathcomp(div ssrnum ssrint rat prime path binomial) mathcomp(tuple finset) gaia(fibm)