proposition: Lemma leqDmod m n d : 0 < d -> (d <= m %% d + n %% d) = ((m + n) %% d < n %% d).
proof: Proof. move=> d_gt0; rewrite modnD//. have [d_le|_] := leqP d; last by rewrite subn0 ltnNge leq_addl. by rewrite -(ltn_add2r d) mul1n (subnK d_le) addnC ltn_add2l ltn_pmod. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq)