Euclid's division lemma

Stream: Is there code for X?

[Ben]

Is there a proof of "Euclid's division lemma" in mathlib? I couldn't find one.
I started something, I think it would be like:

def int.to_pos : int → nat
| (int.of_nat n) := n
| (int.neg_succ_of_nat n) := n

lemma euclid_division (a b: int) (b_ne_zero: b ≠ 0)
  : ∃! q:int, ∃! r: fin (int.to_pos b), a = b * q + r.val := sorry

Does this exists already under a different name?

[Johan Commelin]

I think that #reduce int.to_pos (-3) does not give the result you expect.

[Johan Commelin]

You probably want int.nat_abs.

[Johan Commelin]

I think that the lemma you are looking for is somewhere close to docs#int.mod.

[Johan Commelin]

docs#int.div_add_mod

[Ben]

Johan Commelin said:

You probably want int.nat_abs.

Ah yes that is better, I forgot about the how -0 isn't covered. #eval (int.to_pos (-3)) would then return 2. int.nat_abs was what I was looking for :thumbs_up: