case refl
n : ℕ
⊢ 5 ≤ fib 5

case step
n✝ n : ℕ
five_le_n : Nat.le 5 n
IH : n ≤ fib n
⊢ succ n ≤ fib (succ n)
n : ℕ
five_le_n : 5 ≤ n
⊢ n ≤ fib n
induction' five_le_n with n five_le_n IH
no goals
case refl
n : ℕ
⊢ 5 ≤ fib 5
rfl
case step
n✝ n : ℕ
five_le_n : Nat.le 5 n
IH : n ≤ fib n
⊢ n < fib (succ n)
case step
n✝ n : ℕ
five_le_n : Nat.le 5 n
IH : n ≤ fib n
⊢ succ n ≤ fib (succ n)
rw [succ_le_iff]
no goals
case step
n✝ n : ℕ
five_le_n : Nat.le 5 n
IH : n ≤ fib n
⊢ n < fib (succ n)
calc
  n ≤ fib n := IH
  _ < fib (n + 1) := fib_lt_fib_succ (le_trans (by decide) five_le_n)
no goals
n✝ n : ℕ
five_le_n : Nat.le 5 n
IH : n ≤ fib n
⊢ 2 ≤ 5
decide