How to prove that x < y → x ≤ y - 2 if both are odd or both are even in Lean?

Question

I'm working my way through tutorials and also formalizing mathematics course and trying to solve other problems I find interesting. There is surprisingly little examples with inequalities.

How one can prove that if two ℤ numbers are both even or both odd, the closest they can be if not equal is 2 apart?

import data.int.basic
import data.int.parity

theorem even_even_at_least_two_apart { x y : ℤ } : even x ∧ even y → x < y → x ≤ y - 2 :=
begin
  sorry
end

I'm having trouble converting from mod to minimal differences. Or I'm stuck with x ≤ y - 1 that can be obtained from lt. I suspect my initial formalization can be off.

This is as far as i can get:

  rintros ⟨ hx, hy ⟩ hlt,
  rw int.even_iff at hx hy,
  rw ← int.le_sub_one_iff at hlt,

Answer 1

Using library_search and linarith can save you a lot of trouble. The lines ending with the comment -- library_search where found using library_search.

import data.int.parity
import tactic.linarith

theorem even_even_at_least_two_apart { x y : ℤ } : even x ∧ even y → x < y → x ≤ y - 2 :=
begin
  rintros ⟨hx, hy⟩ hxy,
  have h₁ : even (y - x),
  exact int.even.sub_even hy hx,  -- library_search,
  have h₂ : 0 < y - x,
  exact sub_pos.mpr hxy, -- library_search
  rcases h₁ with ⟨k, hk⟩,
  rw hk at *,
  have : 1 ≤ k, by linarith,
  linarith
end

Note that the statement would be nicer to read and use as

theorem even_even_at_least_two_apart {x y : ℤ} (hx : even x) (hy : even y) (hxy : x < y) :
  x ≤ y - 2