proposition: Lemma divnMl p m d : p > 0 -> p * m %/ (p * d) = m %/ d.
proof: Proof. move=> p_gt0; have [->|d_gt0] := posnP d; first by rewrite muln0. rewrite [RHS]/divn; case: edivnP; rewrite d_gt0 /= => q r ->{m} lt_rd. rewrite mulnDr mulnCA divnMDl; last by rewrite muln_gt0 p_gt0. by rewrite addnC divn_small // ltn_pmul2l. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq)