case zero
m : ℕ
⊢ ↑(-1) = zero

case succ
m n✝ : ℕ
⊢ ↑(-1) = Nat.succ n✝
n m : ℕ
⊢ ↑(-1) = n
cases n
case succ
m n✝ : ℕ
⊢ n✝ + 1 < Nat.succ n✝ + 1
case succ
m n✝ : ℕ
⊢ ↑(-1) = Nat.succ n✝
rw [Fin.coe_neg, Fin.val_one, Nat.succ_sub_one, Nat.mod_eq_of_lt]
no goals
case succ
m n✝ : ℕ
⊢ n✝ + 1 < Nat.succ n✝ + 1
constructor
no goals
case zero
m : ℕ
⊢ ↑(-1) = zero
simp