equivalent formulation of "is not divisible"

Stream: Is there code for X?

[Floris van Doorn]

Is this in mathlib? I need the direction from right to left.

lemma not_dvd_iff (n m : ℕ) : ¬ n ∣ m ↔ ∃ k, n * k < m ∧ m < n * (k + 1)

[Johan Commelin]

I don't recognise it