proposition: Lemma divnMA m n p : m %/ (n * p) = m %/ n %/ p.
proof: Proof. case: n p => [|n] [|p]; rewrite ?muln0 ?div0n //. rewrite [in RHS](divn_eq m (n.+1 * p.+1)) mulnA mulnAC !divnMDl //. by rewrite [_ %/ p.+1]divn_small ?addn0 // ltn_divLR // mulnC ltn_mod. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq)