proposition: Lemma divzMDl q m d : d != 0 -> ((q * d + m) %/ d)%Z = q + (m %/ d)%Z.
proof: Proof. rewrite Order.TotalTheory.neq_lt -oppr_gt0 => nz_d. wlog{nz_d} d_gt0: q d / d > 0; last case: d => // d in d_gt0 *. move=> IH; case/orP: nz_d => /IH// /(_ (- q)). by rewrite mulrNN !divzN -opprD => /oppr_inj. wlog q_gt0: q m / q >= 0; last case: q q_gt0 => // q _. move=> IH; case: q => n; first exact: IH; rewrite NegzE mulNr. by apply: canRL (addKr _) _; rewrite -IH ?addNKr. case: m => n; first by rewrite !divz_nat divnMDl. have [le_qd_n | lt_qd_n] := leqP (q * d) n. rewrite divNz_nat // NegzE -(subnKC le_qd_n) divnMDl //. by rewrite -!addnS !PoszD !opprD !addNKr divNz_nat. rewrite divNz_nat // NegzE -PoszM subzn // divz_nat. apply: canRL (addrK _) _; congr _%:Z; rewrite addnC -divnMDl // mulSnr. rewrite -{3}(subnKC (ltn_pmod n d_gt0)) addnA addnS -divn_eq addnAC. by rewrite subnKC // divnMDl // divn_small ?addn0 // subnSK ?ltn_mod ?leq_subr. 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)