mathlib3

3b971a7b - feat(data/zmod/basic): Add `zmod.cast_sub_one` (#13889)

feat(data/zmod/basic): Add `zmod.cast_sub_one` (#13889) This PR adds `zmod.cast_sub_one`, an analog of `fin.coe_sub_one`. Unfortunately, the proof is a bit long. But maybe it can be golfed? Co-authored-by: tb65536 <tb65536@users.noreply.github.com>