case inl
a b : ℤ
n : ℕ
t : ℤ
hst : 0 ∣ t
⊢ t / 0 ∣ t

case inr
a b : ℤ
n : ℕ
s t : ℤ
hst : s ∣ t
hs : s ≠ 0
⊢ t / s ∣ t
a b : ℤ
n : ℕ
s t : ℤ
hst : s ∣ t
⊢ t / s ∣ t
rcases eq_or_ne s 0 with (rfl | hs)
case inr.intro
a b : ℤ
n : ℕ
s t : ℤ
hs : s ≠ 0
c : ℤ
hc : t = s * c
⊢ t / s ∣ t
case inr
a b : ℤ
n : ℕ
s t : ℤ
hst : s ∣ t
hs : s ≠ 0
⊢ t / s ∣ t
rcases hst with ⟨c, hc⟩
no goals
case inr.intro
a b : ℤ
n : ℕ
s t : ℤ
hs : s ≠ 0
c : ℤ
hc : t = s * c
⊢ t / s ∣ t
simp [hc, Int.mul_ediv_cancel_left _ hs]
no goals
case inl
a b : ℤ
n : ℕ
t : ℤ
hst : 0 ∣ t
⊢ t / 0 ∣ t
simpa using hst