proposition: Lemma edivnB m n d (offset := m %% d < n %% d) : 0 < d -> n <= m -> edivn (m - n) d = (m %/ d - n %/ d - offset, offset * d + m %% d - n %% d).
proof: Proof. by move=> d_gt0 le_nm; rewrite edivn_def divnB// modnB. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq)