## Stream: maths

### Topic: uniqueness of division and remainder

#### Kevin Buzzard (Nov 04 2019 at 13:22):

Do we have anything like this

example (a q b r : ℤ) (hb : b > 0) : a = r + b * q → 0 ≤ r → r < b → r = a % b := sorry


in mathlib already? One could also prove q = a / b. I can prove them, I just don't want to.

Related: if b > 0 is an integer and 0 <= r < b is a multiple of b then r = 0. Do we have this?

#### Chris Hughes (Nov 04 2019 at 13:23):

I remember something called div_mod_unique. It might only be for nat.

#### Kevin Buzzard (Nov 04 2019 at 13:23):

Well remembered and yes it's only for nat, so it seems. Thanks.

#### Kevin Buzzard (Nov 04 2019 at 13:26):

protected theorem div_mod_unique {n k m d : ℕ} (h : 0 < k) :
n / k = d ∧ n % k = m ↔ m + k * d = n ∧ m < k :=


What are the chances that the user has those facts in exactly that way so they can rewrite? Both sides have an \and :-/ The int version will have the additional hypothesis that m>=0 as well :-/

#### Mario Carneiro (Nov 04 2019 at 13:38):

it's not for rewriting like that, but you can always rewrite with ((div_mod_unique h1).2 <h2, h3>).2

#### Kevin Buzzard (Nov 04 2019 at 15:49):

Fair point.

Last updated: May 11 2021 at 16:22 UTC