proposition: Lemma ltn_mod2r p m n : p > 0 -> m %/ p = n %/ p -> m %% p < n %% p -> m < n.
proof: Proof. move=> p_gt0 eq_div lt_mod; rewrite (divn_eq m p) (divn_eq n p). by rewrite {}eq_div ltn_add2l in lt_mod *. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice fintype tuple) mathcomp(bigop finset finfun perm fingraph path div) bigmin