Nat.div_lt_of_lt_mul

theorem Nat.div_lt_of_lt_mul : ∀ {m n k : ℕ}, m < n * k → m / n < k

This theorem states that for any three natural numbers `m`, `n`, and `k`, if `m` is less than the product of `n` and `k`, then the integer division of `m` by `n` is less than `k`. In other words, this theorem establishes a relationship between multiplication and division in the context of less-than comparisons in natural numbers.

More concisely: If `m` < `n` * `k` in the natural numbers, then `m / n` < `k`.