case intro
m k✝ l k : ℕ
h1 : 0 < m * k
h2 : m * k < m
⊢ False
m n k l : ℕ
h1 : 0 < n
h2 : n < m
⊢ ¬m ∣ n
rintro ⟨k, rfl⟩
case intro.inl
m k l : ℕ
h1 : 0 < m * 0
h2 : m * 0 < m
⊢ False

case intro.inr
m k✝ l k : ℕ
h1 : 0 < m * k
h2 : m * k < m
hk : k > 0
⊢ False
case intro
m k✝ l k : ℕ
h1 : 0 < m * k
h2 : m * k < m
⊢ False
rcases Nat.eq_zero_or_pos k with (rfl | hk)
no goals
case intro.inl
m k l : ℕ
h1 : 0 < m * 0
h2 : m * 0 < m
⊢ False
exact lt_irrefl 0 h1
no goals
case intro.inr
m k✝ l k : ℕ
h1 : 0 < m * k
h2 : m * k < m
hk : k > 0
⊢ False
exact not_lt.2 (le_mul_of_pos_right hk) h2