proposition: Lemma edivnD m n d (offset := m %% d + n %% d >= d) : 0 < d -> edivn (m + n) d = (m %/ d + n %/ d + offset, m %% d + n %% d - offset * d).
proof: Proof. rewrite {}/offset; case: d => // d _; rewrite /divn !modn_def. case: (edivnP m d.+1) (edivnP n d.+1) => [/= q r -> r_lt] [/= p s -> s_lt]. rewrite addnACA -mulnDl; have [r_le s_le] := (ltnW r_lt, ltnW s_lt). have [d_ge|d_lt] := leqP; first by rewrite addn0 mul0n subn0 edivn_eq. rewrite addn1 mul1n -[in LHS](subnKC d_lt) addnA -mulSnr edivn_eq//. by rewrite ltn_subLR// -addnS leq_add. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq)