case intro.intro
m n k a b : ℕ
h : n * a < n * b + n
⊢ n * a ≤ n * b
a b m n k : ℕ
h : a < b + n
⊢ n ∣ a → n ∣ b → a ≤ b
rintro ⟨a, rfl⟩ ⟨b, rfl⟩
case intro.intro
m n k a b : ℕ
h : n * a < n * (b + 1)
⊢ n * a ≤ n * b
case intro.intro
m n k a b : ℕ
h : n * a < n * b + n
⊢ n * a ≤ n * b
rw [← mul_add_one n] at h
no goals
case intro.intro
m n k a b : ℕ
h : n * a < n * (b + 1)
⊢ n * a ≤ n * b
exact mul_le_mul_left' (lt_succ_iff.1 <| lt_of_mul_lt_mul_left h bot_le) _