n m i : ℕ
h : i < n
⊢ 0 < ↑{ val := Nat.succ i, isLt := (_ : i + 1 < n + 1) }
n m i : ℕ
h : i < n
⊢ 0 < { val := Nat.succ i, isLt := (_ : i + 1 < n + 1) }
rw [lt_iff_val_lt_val, val_zero]
no goals
n m i : ℕ
h : i < n
⊢ 0 < ↑{ val := Nat.succ i, isLt := (_ : i + 1 < n + 1) }
exact Nat.succ_pos i