proposition: Lemma modnB m n d : 0 < d -> n <= m -> (m - n) %% d = (m %% d < n %% d) * d + m %% d - n %% d.
proof: Proof. move=> d_gt0 nm; rewrite -[in m %% _](subnK nm) -leqDmod// modnD//. have [d_le|_] := leqP d; last by rewrite mul0n add0n subn0 addnK. by rewrite mul1n addnBA// addnC !addnK. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq)