v % 2 ≠ (v + 1) % 2

Stream: Is there code for X?

[Iván Renison]

Is there any theorem that says this?

theorem aux (n : ℕ) : n % 2 ≠ (n + 1) % 2 := by
  sorry

[Ruben Van de Velde]

A bit annoying:

theorem aux (n : ℕ) : n % 2 ≠ (n + 1) % 2 := by
  rw [Nat.add_mod]
  have := Nat.mod_lt n two_pos
  interval_cases n % 2 <;> simp

[Ruben Van de Velde]

Maybe more conceptual? Not sure

theorem aux' (n : ℕ) : n % 2 = if Even n then 0 else 1 := by
  simp_rw [Nat.even_iff]
  have := Nat.mod_lt n two_pos
  interval_cases n % 2 <;> simp

theorem aux (n : ℕ) : n % 2 ≠ (n + 1) % 2 := by
  rw [aux', aux']
  simp_rw [Nat.even_add_one]
  split_ifs <;> simp

[Eric Wieser]

theorem aux (n : ℕ) : n % 2 ≠ (n + 1) % 2 := by
  refine (ZMod.eq_iff_modEq_nat 2).not.mp ?_
  simp

[Iván Renison]

Thanks