case zero
n m : ℕ
i : Fin (Nat.succ zero)
h : i < last zero
⊢ ↑(i + 1) = ↑i + 1

case succ
n m n✝ : ℕ
i : Fin (Nat.succ (Nat.succ n✝))
h : i < last (Nat.succ n✝)
⊢ ↑(i + 1) = ↑i + 1
n✝ m n : ℕ
i : Fin (Nat.succ n)
h : i < last n
⊢ ↑(i + 1) = ↑i + 1
cases n
n m n✝ : ℕ
i : Fin (Nat.succ (Nat.succ n✝))
h : i < last (Nat.succ n✝)
⊢ ↑i < n✝ + 1
case succ
n m n✝ : ℕ
i : Fin (Nat.succ (Nat.succ n✝))
h : i < last (Nat.succ n✝)
⊢ ↑(i + 1) = ↑i + 1
rw [Fin.val_add, Fin.val_one, Nat.mod_eq_of_lt (Nat.succ_lt_succ _)]
no goals
n m n✝ : ℕ
i : Fin (Nat.succ (Nat.succ n✝))
h : i < last (Nat.succ n✝)
⊢ ↑i < n✝ + 1
exact h
no goals
case zero
n m : ℕ
i : Fin (Nat.succ zero)
h : i < last zero
⊢ ↑(i + 1) = ↑i + 1
cases h