proposition: Lemma ltn_divLR m n d : d > 0 -> (m %/ d < n) = (m < n * d).
proof: Proof. move=> d_gt0; apply/idP/idP. by rewrite -(leq_pmul2r d_gt0); apply: leq_trans (ltn_ceil _ _). rewrite !ltnNge -(@leq_pmul2r d n) //; apply: contra => le_nd_floor. exact: leq_trans le_nd_floor (leq_trunc_div _ _). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq)