case zero
m : ℕ
i : Fin (zero + 1)
h : i < last zero
⊢ 0 < i + 1

case succ
m n✝ : ℕ
i : Fin (Nat.succ n✝ + 1)
h : i < last (Nat.succ n✝)
⊢ 0 < i + 1
n m : ℕ
i : Fin (n + 1)
h : i < last n
⊢ 0 < i + 1
cases n
no goals
case zero
m : ℕ
i : Fin (zero + 1)
h : i < last zero
⊢ 0 < i + 1
exact absurd h (Nat.not_lt_zero _)
case succ
m n✝ : ℕ
i : Fin (Nat.succ n✝ + 1)
h✝ : ↑i < Nat.succ n✝
h : ↑i + 1 < Nat.succ n✝ + 1
⊢ 0 < i + 1
case succ
m n✝ : ℕ
i : Fin (Nat.succ n✝ + 1)
h : i < last (Nat.succ n✝)
⊢ 0 < i + 1
rw [lt_iff_val_lt_val, val_last, ← add_lt_add_iff_right 1] at h
case succ
m n✝ : ℕ
i : Fin (Nat.succ n✝ + 1)
h✝ : ↑i < Nat.succ n✝
h : ↑i + 1 < Nat.succ n✝ + 1
⊢ 0 < ↑i + 1
case succ
m n✝ : ℕ
i : Fin (Nat.succ n✝ + 1)
h✝ : ↑i < Nat.succ n✝
h : ↑i + 1 < Nat.succ n✝ + 1
⊢ 0 < i + 1
rw [lt_iff_val_lt_val, val_add, val_zero, val_one, Nat.mod_eq_of_lt h]
no goals
case succ
m n✝ : ℕ
i : Fin (Nat.succ n✝ + 1)
h✝ : ↑i < Nat.succ n✝
h : ↑i + 1 < Nat.succ n✝ + 1
⊢ 0 < ↑i + 1
exact Nat.zero_lt_succ _