a✝ b m n✝ k n a : ℕ
ha : 0 < a
han : ¬a ∣ n
⊢ a * (n / a) ≠ n
a✝ b m n✝ k n a : ℕ
ha : 0 < a
⊢ (∃ k, a * k < n ∧ n < a * (k + 1)) ↔ ¬a ∣ n
refine'
  ⟨fun ⟨k, hk1, hk2⟩ => not_dvd_of_between_consec_multiples hk1 hk2, fun han =>
    ⟨n / a, ⟨lt_of_le_of_ne (mul_div_le n a) _, lt_mul_div_succ _ ha⟩⟩⟩
no goals
a✝ b m n✝ k n a : ℕ
ha : 0 < a
han : ¬a ∣ n
⊢ a * (n / a) ≠ n
exact mt (Dvd.intro (n / a)) han