proposition: Lemma modn_divl m n d : (m %/ d) %% n = m %% (n * d) %/ d.
proof: Proof. case: d n => [|d] [|n] //; rewrite [in LHS]/divn [in LHS]modn_def. case: (edivnP m d.+1) edivnP => [/= _ r -> le_rd] [/= q s -> le_sn]. rewrite mulnDl -mulnA -addnA modnMDl modn_small ?divnMDl ?divn_small ?addn0//. by rewrite mulSnr -addnS leq_add ?leq_mul2r. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq)