case zero
m : ℕ
a : Fin zero
⊢ ↑castSucc a + 1 = succ a

case succ
m n✝ : ℕ
a : Fin (Nat.succ n✝)
⊢ ↑castSucc a + 1 = succ a
n m : ℕ
a : Fin n
⊢ ↑castSucc a + 1 = succ a
cases n
no goals
case zero
m : ℕ
a : Fin zero
⊢ ↑castSucc a + 1 = succ a
exact @finZeroElim (fun _ => _) a
no goals
case succ
m n✝ : ℕ
a : Fin (Nat.succ n✝)
⊢ ↑castSucc a + 1 = succ a
simp [a.is_lt, eq_iff_veq, add_def, Nat.mod_eq_of_lt]