case inl
a✝ b m n✝ k n a : ℕ
hnd : 0 ∣ n
⊢ a < n / 0 ↔ 0 * a < n

case inr
a✝ b m n✝ k n d : ℕ
hnd : d ∣ n
a : ℕ
hd0 : d > 0
⊢ a < n / d ↔ d * a < n
a✝ b m n✝ k n d : ℕ
hnd : d ∣ n
a : ℕ
⊢ a < n / d ↔ d * a < n
rcases d.eq_zero_or_pos with (rfl | hd0)
no goals
case inr
a✝ b m n✝ k n d : ℕ
hnd : d ∣ n
a : ℕ
hd0 : d > 0
⊢ a < n / d ↔ d * a < n
rw [← mul_lt_mul_left hd0, ← Nat.eq_mul_of_div_eq_right hnd rfl]
no goals
case inl
a✝ b m n✝ k n a : ℕ
hnd : 0 ∣ n
⊢ a < n / 0 ↔ 0 * a < n
simp [zero_dvd_iff.mp hnd]