n : ℕ
⊢ fib (n + 2) < fib (n + 1 + 2)
⊢ StrictMono fun n => fib (n + 2)
refine' strictMono_nat_of_lt_succ fun n => _
n : ℕ
⊢ fib (n + 2) < fib (n + 2 + 1)
n : ℕ
⊢ fib (n + 2) < fib (n + 1 + 2)
rw [add_right_comm]
no goals
n : ℕ
⊢ fib (n + 2) < fib (n + 2 + 1)
exact fib_lt_fib_succ (self_le_add_left _ _)