k n m : Nat
lo : 0 ≤ m
hi : m < 0
hn : n = 0
⊢ False
k n m : Nat
lo : k * n ≤ m
hi : m < succ k * n
hn : n = 0
⊢ False
rw [hn, Nat.mul_zero] at hi lo
no goals
k n m : Nat
lo : 0 ≤ m
hi : m < 0
hn : n = 0
⊢ False
exact absurd lo (Nat.not_le_of_gt hi)