uniqueness of division and remainder

Stream: maths

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

Fair point.