simp only [dvd_mul_right]
x : ℤ
hlt : -24 < 3 * x
hlt' : 3 * x < 24
m7 : ¬x = -7
m6 : ¬x = -6
m5 : ¬x = -5
m4 : ¬x = -4
m3 : ¬x = -3
m2 : ¬x = -2
m1 : ¬x = -1
z : ¬x = 0
p1 : ¬x = 1
p2 : ¬x = 2
p3 : ¬x = 3
p4 : ¬x = 4
p5 : ¬x = 5
p6 : ¬x = 6
p7 : ¬x = 7
this : 24 = 3 * 8
⊢ 3 ∣ 3 * 8
no goals