proposition: Lemma divzMA_ge0 m n p : n >= 0 -> (m %/ (n * p) = (m %/ n)%Z %/ p)%Z.
proof: Proof. case: n => // [[|n]] _; first by rewrite mul0r !divz0 div0z. wlog p_gt0: p / p > 0; last case: p => // p in p_gt0 *. by case/intP: p => [|p|p] IH; rewrite ?mulr0 ?divz0 ?mulrN ?divzN // IH. rewrite {2}(divz_eq m (n.+1%:Z * p)) mulrA mulrAC !divzMDl // ?Order.POrderTheory.gt_eqF //. rewrite [rhs in _ + rhs]divz_small ?addr0 // ltz_divLR // divz_ge0 //. by rewrite mulrC ltz_pmod ?modz_ge0 ?Order.POrderTheory.gt_eqF ?pmulr_lgt0. 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)