case intro
n k l d : ℕ
h1 : n * k < n * d
h2 : n * d < n * (k + 1)
⊢ False
m n k l : ℕ
h1 : n * k < m
h2 : m < n * (k + 1)
⊢ ¬n ∣ m
rintro ⟨d, rfl⟩
no goals
case intro
n k l d : ℕ
h1 : n * k < n * d
h2 : n * d < n * (k + 1)
⊢ False
exact Monotone.ne_of_lt_of_lt_nat (Covariant.monotone_of_const n) k h1 h2 d rfl