proposition: Lemma divnD m n d : 0 < d -> (m + n) %/ d = (m %/ d) + (n %/ d) + (m %% d + n %% d >= d).
proof: Proof. by move=> /(@edivnD m n); rewrite edivn_def => -[]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq)