simple calculations in `ZMod q`

Stream: Is there code for X?

[Moritz Firsching]

When using docs#orderOf_eq_prime for something I need the lemma one_ne_two as described here:

import Mathlib.Tactic

lemma ZMod.zero_ne_one (q : ℕ) [Fact (1 < q)] : (0 : ZMod q) ≠ 1 := by
  intro h
  have := ZMod.val_one q ▸ (ZMod.val_eq_zero (1 : ZMod q)).mpr h.symm
  linarith

lemma ZMod.one_ne_two (q : ℕ)  [Fact (1 < q)] : (1 : ZMod q) ≠ 2 := by
  intro h1
  have h : (2 - 1 : ZMod q) = 0 := by exact (sub_eq_zero.mpr h1.symm)
  norm_num at h
  exact (ZMod.zero_ne_one q) h.symm

I feel like something like this should be in the library, is there?
Or maybe there is a tactic to deal with these kind of trivial calculations in ZMod q when q is larger than 1.

[Ruben Van de Velde]

Maybe there's more API assuming NeZero q? I'm not sure

Doh

[Kevin Buzzard]

Both lemmas also need q!=1

[Eric Wieser]

Both lemmas only need q ≠ 1