@[simp]

theorem ZMod.val_mk {q : ℕ} (n : ℕ) (hn : n < q + 1) : val ⟨n, hn⟩ = n

@[simp]

theorem ZMod.mk_eq_natCast {q : ℕ} (n : ℕ) (hn : n < q + 1) : ⟨n, hn⟩ = ↑n