theorem Int.even_iff_exi {n : ℤ} : Even n ↔ ∃ (k : ℤ), n = k * 2

theorem Int.odd_iff_exi {n : ℤ} : Odd n ↔ ∃ (k : ℤ), n = k * 2 + 1

theorem Int.mod_2_ind {P : ℤ → Prop} (h₁ : ∀ (n : ℤ), P (n * 2)) (h₂ : ∀ (n : ℤ), P (n * 2 + 1)) (n : ℤ) : P n

theorem Int.not_even_mul_2_succ {n : ℤ} : ¬Even (n * 2 + 1)

@[simp]

theorem Int.not_odd_mul_2 {n : ℤ} : ¬Odd (n * 2)

theorem Int.le_one_iff {n : ℤ} (h : 0 ≤ n) : n ≤ 1 ↔ n = 0 ∨ n = 1

theorem Int.of_between_succ {a b : ℤ} (h₁ : a ≤ b) (h₂ : b ≤ a + 1) : b = a ∨ b = a + 1

theorem Int.add_div_eq {a b : ℤ} (h : 0 < b) : (a + b) / b = a / b + 1

@[simp]

theorem Int.negSucc_succ {n : ℕ} : negSucc (n + 1) = negSucc n - 1

@[simp]

theorem Int.even_succ_iff {n : ℤ} : Even (n + 1) ↔ Odd n

@[simp]

theorem Int.odd_succ_iff {n : ℤ} : Odd (n + 1) ↔ Even n

theorem Int.succ_div_2_eq_div_iff {n : ℤ} (hp : 0 ≤ n) : (n + 1) / 2 = n / 2 ↔ Even n

theorem Int.succ_div_2_eq_div_succ_iff {n : ℤ} (hp : 0 ≤ n) : (n + 1) / 2 = n / 2 + 1 ↔ Odd n

theorem Int.succ_div_2_eq_or_eq {n : ℤ} (hp : 0 ≤ n) : (n + 1) / 2 = n / 2 ∨ (n + 1) / 2 = n / 2 + 1

theorem Int.succ_div_2_eq_div_iff' {n : ℤ} (hp : 0 ≤ n) : n / 2 = (n + 1) / 2 ↔ Even n

@[simp]

theorem Int.succ_div_2_eq_div_succ_iff' {n : ℤ} (hp : 0 ≤ n) : n / 2 + 1 = (n + 1) / 2 ↔ Odd n

theorem Int.mul_2_succ_div_2_eq {n : ℤ} (hp : 0 ≤ n) : (n * 2 + 1) / 2 = n

@[simp]

theorem Int.max_abs_eq_zero_iff {n m : ℤ} : max |n| |m| = 0 ↔ n = 0 ∧ m = 0

@[simp]

theorem Int.eq_self_sub_iff {a b : ℤ} : a = a - b ↔ b = 0

theorem Int.toNat_eq_self_of {z : ℤ} (h₁ : 0 ≤ z) : ↑z.toNat = z