Int/Nat conversions

Stream: new members

[Alex Gu]

I am trying to prove this theorem:

theorem no_solution_in_positive_integers :
  ¬ ∃ (x y : ℤ), x > 0 ∧ y > 0 ∧ x^2006 - 4 * y^2006 - 2006 = 4 * y^2007 + 2007 * y := by
  intro h
  obtain ⟨x, y, hx, hy, heq⟩ := h
  have mod_4_congruence : (4 * y^2006 + 2007) % 4 = 3 := by sorry

If x, y were natural numbers (which they are), I could complete the sorry with rw [Nat.add_mod]; simp. However, they are defined here as integers, so I'm wondering if there's any way to complete the sorry without needing to change the problem statement to natural numbers?

[Aaron Liu]

May I interest you in docs#Int.add_emod

[Ilmārs Cīrulis]

omega works here too, it seems

[Alex Gu]

haha nice, thx! what is the e in emod

[Aaron Liu]

From the docstring of docs#Int.emod:

Integer modulus that uses the E-rounding convention. Usually accessed via the % operator.

In the E-rounding convention (Euclidean division), Int.emod x y satisfies 0 ≤ Int.emod x y < Int.natAbs y for y ≠ 0 and Int.ediv is the unique function satisfying Int.emod x y + (Int.ediv x y) * y = x for y ≠ 0.

This function is overridden by the compiler with an efficient implementation. This definition is the logical model.

Examples:

• (7 : Int) % (0 : Int) = 7
• (0 : Int) % (7 : Int) = 0
• (12 : Int) % (6 : Int) = 0
• (12 : Int) % (-6 : Int) = 0
• (-12 : Int) % (6 : Int) = 0
• (-12 : Int) % (-6 : Int) = 0
• (12 : Int) % (7 : Int) = 5
• (12 : Int) % (-7 : Int) = 5
• (-12 : Int) % (7 : Int) = 2
• (-12 : Int) % (-7 : Int) = 2