divisor dividend and remained for nat

Stream: Is there code for X?

[Yakov Pechersky]

What's the mathlib name for this?

example (x y : ℕ) : ∃ (m k : ℕ) (hk : k < y), x = m * y + k :=
sorry

[Johan Commelin]

I don't think mathlib has that as an existential. But there is docs#nat.mod_add_div

[Johan Commelin]

And certainly also docs#nat.mod_lt