proposition: Lemma ltn_div2r p m n : p > 0 -> m %/ p < n %/ p -> m < n.
proof: Proof. move=> p_gt0 lt_div; rewrite (divn_eq m p) (divn_eq n p). rewrite -(subnKC lt_div) mulnDl mulSn -!addnA addnCA ltn_add2l. by rewrite (leq_trans (ltn_pmod _ _)) // leq_addr. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice fintype tuple) mathcomp(bigop finset finfun perm fingraph path div) bigmin