proposition: Lemma geq_divBl k m p : k %/ p - m %/ p <= (k - m) %/ p + 1.
proof: Proof. rewrite leq_subLR addnA; apply: leq_trans (leq_divDl _ _ _). by rewrite -maxnE leq_div2r ?leq_maxr. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq)