proposition: Lemma edivnS m d : 0 < d -> edivn m.+1 d = if d %| m.+1 then ((m %/ d).+1, 0) else (m %/ d, (m %% d).+1).
proof: Proof. case: d => [|[|d]] //= _; first by rewrite edivn_def modn1 dvd1n !divn1. rewrite -addn1 /dvdn modn_def edivnD//= (@modn_small 1)// (@divn_small 1)//. rewrite addn1 addn0 ltnS; have [||<-] := ltngtP d.+1. - by rewrite ltnNge -ltnS ltn_pmod. - by rewrite addn0 mul0n subn0. - by rewrite addn1 mul1n subnn. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq)