## Stream: Is there code for X?

### Topic: divisor dividend and remained for nat

#### Yakov Pechersky (Apr 05 2021 at 16:56):

What's the mathlib name for this?

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


#### Johan Commelin (Apr 05 2021 at 16:59):

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

#### Johan Commelin (Apr 05 2021 at 16:59):

And certainly also docs#nat.mod_lt

Last updated: May 07 2021 at 21:10 UTC