cast from `ℕ` to `ZMod p` after adding or subtracting p

Stream: Is there code for X?

[Moritz Firsching]

I'm proving a theorem looking at descFactorial mod p and find myself needing a lemma, which i called cast_self_sub below.

import Mathlib.Data.ZMod.Basic
import Mathlib.Data.Nat.Factorial.BigOperators

set_option autoImplicit false
open Nat BigOperators Finset

theorem cast_self_sub {n p : ℕ} (h : n ≤ p) : ((p - n) : ℕ) = - (n : ZMod p) := by
  rw [Nat.cast_sub h, CharP.cast_eq_zero, zero_sub]

variable (α  β : Type) (s : Finset α) (f: α →  β)
variable [CommMonoid β]

@[to_additive card_nsmul_add_sum]
theorem pow_card_mul_prod {b : β} : b ^ s.card * ∏ a in s, f a = ∏ a in s, b * f a :=
  (prod_const b).symm ▸ prod_mul_distrib.symm

theorem descFactorialZMod (n p : ℕ) (h : n ≤ p) :
    (descFactorial (p - 1) n : ZMod p) = (-1) ^ n * n ! := by
  rw [descFactorial_eq_prod_range, ← prod_range_add_one_eq_factorial]
  simp only [cast_prod]
  nth_rw 2 [← card_range n]
  rw [pow_card_mul_prod]
  refine prod_congr rfl ?_
  intro x hx
  rw [← tsub_add_eq_tsub_tsub_swap p x 1, cast_self_sub <|
      Nat.lt_of_lt_of_le (List.mem_range.mp hx) h, cast_succ, neg_add_rev]
  ring_nf

Seems like cast_self_sub and its cousins:

theorem cast_sub_self {n p : ℕ } (h : p ≤ n) : ((n - p) : ℕ) = (n : ZMod p) := by
  rw [Nat.cast_sub h, ZMod.nat_cast_self p, sub_zero]

theorem cast_self_add (i p : ℕ) : ((p + i) : ℕ) = (i : ZMod p) := by
  rw [Nat.cast_add, CharP.cast_eq_zero, zero_add]

theorem cast_add_self (i p : ℕ) : ((i + p) : ℕ) = (i : ZMod p) := by
  rw [Nat.cast_add, ZMod.nat_cast_self p, add_zero]

might be useful. Are they already in mathlib perhaps in suitably generalized form? If not, would this be a good addition?