x ≠ (x + 1) % n

Stream: Is there code for X?

[Iván Renison]

Is there code for this?

theorem aux (x n : ℕ) (hx : x < n) (hn : 2 ≤ n) : x ≠ (x + 1) % n :=
  sorry

[Ruben Van de Velde]

import Mathlib
theorem aux (x n : ℕ) (hx : x < n) (hn : 2 ≤ n) : x ≠ (x + 1) % n := by
  rw [← Nat.add_one_le_iff] at hx
  cases hx.eq_or_lt with
  | inl hx =>
    subst hx
    simp
    omega
  | inr hx =>
    rw [Nat.mod_eq_of_lt hx]
    omega

Not sure if there's anything better, the conclusion seems pretty specific

[Iván Renison]

Thanks

[Iván Renison]

And would it be a good addition to mathlib, or it's to specific?

[Daniel Weber]

you don't actually need hx:

import Mathlib
theorem aux (x n : ℕ) (hn : 2 ≤ n) : x ≠ (x + 1) % n := by
  apply_fun (· % n)
  simp only [dvd_refl, Nat.mod_mod_of_dvd, ne_eq]
  exact fun h ↦
    Nat.not_succ_le_self 1 <| hn.trans <| Nat.le_of_dvd zero_lt_one <|
    Nat.dvd_of_mod_eq_zero <| Nat.add_sub_self_left x 1 ▸ Nat.sub_mod_eq_zero_of_mod_eq h.symm

[Michael Stoll]

theorem aux (x n : ℕ) (hn : 2 ≤ n) : x ≠ (x + 1) % n := by
  apply_fun (· % n)
  simp only [dvd_refl, Nat.mod_mod_of_dvd, ne_eq, ← ZMod.natCast_eq_natCast_iff', Nat.cast_add,
    self_eq_add_right, ZMod.natCast_zmod_eq_zero_iff_dvd, Nat.dvd_one]
  omega

[Michael Stoll]

theorem aux (x n : ℕ) (hn : 2 ≤ n) : x ≠ (x + 1) % n := by
  apply_fun ((↑) : _ →  ZMod n)
  have : NeZero (1 : ZMod n) := @NeZero.one _ _ <| @ZMod.nontrivial n ⟨hn⟩
  simpa only [ZMod.natCast_mod, Nat.cast_add, Nat.cast_one, ne_eq, self_eq_add_right] using
    one_ne_zero

Going via ZMod n, which I would usually recommend in these situations.