case zero
R : Type u_1
inst✝ : Ring R
⊢ ↑(-1) = ↑Nat.zero - 1

case succ
R : Type u_1
inst✝ : Ring R
n : ℕ
⊢ ↑(-1) = ↑(Nat.succ n) - 1
R : Type u_1
inst✝ : Ring R
n : ℕ
⊢ ↑(-1) = ↑n - 1
cases' n with n
case zero
R : Type u_1
inst✝ : Ring R
⊢ ↑(-1) = ↑0 - 1
case zero
R : Type u_1
inst✝ : Ring R
⊢ ↑(-1) = ↑Nat.zero - 1
dsimp [ZMod, ZMod.cast]
no goals
case zero
R : Type u_1
inst✝ : Ring R
⊢ ↑(-1) = ↑0 - 1
simp
no goals
case succ
R : Type u_1
inst✝ : Ring R
n : ℕ
⊢ ↑(-1) = ↑(Nat.succ n) - 1
rw [← nat_cast_val, val_neg_one, Nat.cast_succ, add_sub_cancel]