proposition: Lemma divnB n m d : 0 < d -> (m - n) %/ d = (m %/ d) - (n %/ d) - (m %% d < n %% d).
proof: Proof. move=> d_gt0; have [mn|/ltnW nm] := leqP m n. by rewrite (eqP mn) (eqP (leq_div2r _ _)) ?div0n. by rewrite -[in m %/ d](subnK nm) divnD// addnAC addnK leqDmod ?subnK ?addnK. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq)