rcases d.eq_zero_or_pos with (rfl | hd0)
n d : Nat
hnd : d ∣ n
a : Nat
⊢ a < n / d ↔ d * a < n
case inl
n a : Nat
hnd : 0 ∣ n
⊢ a < n / 0 ↔ 0 * a < n

case inr
n d : Nat
hnd : d ∣ n
a : Nat
hd0 : d > 0
⊢ a < n / d ↔ d * a < n