case intro
n : ℕ
hn : 2 ≤ 2 + n
⊢ fib (2 + n) < fib (2 + n + 1)
n : ℕ
hn : 2 ≤ n
⊢ fib n < fib (n + 1)
rcases exists_add_of_le hn with ⟨n, rfl⟩
case intro
n : ℕ
hn : 2 ≤ 2 + n
⊢ 0 < fib (n + 1)
case intro
n : ℕ
hn : 2 ≤ 2 + n
⊢ fib (2 + n) < fib (2 + n + 1)
rw [← tsub_pos_iff_lt, add_comm 2, fib_add_two_sub_fib_add_one]
no goals
case intro
n : ℕ
hn : 2 ≤ 2 + n
⊢ 0 < fib (n + 1)
apply fib_pos (succ_pos n)