no goals
n m : ℕ
i : Fin (n + 2)
h : ↑i < n + 1
⊢ 0 < i + 1
exact
(add_one_pos _ (lt_iff_val_lt_val.2 h))
n m : ℕ
i : Fin (n + 2)
h : ↑i < n + 1
⊢ ↑i + 1 < n + 1 + 1
n m : ℕ
i : Fin (n + 2)
h : ↑i < n + 1
⊢ pred (i + 1) (_ : i + 1 ≠ 0) = castLT i h
rw [ext_iff, coe_pred, coe_castLT, val_add, val_one, mod_eq_of_lt, add_tsub_cancel_right]
no goals
n m : ℕ
i : Fin (n + 2)
h : ↑i < n + 1
⊢ ↑i + 1 < n + 1 + 1
exact add_lt_add_right h 1