import Mathlib

-- důkaz fib_n < 2^n
theorem fib_lt_two_pow (n : ℕ) : Nat.fib n < 2 ^ n := by
  induction n using Nat.strong_induction_on with
  | h n ih =>
    match n with
    | 0 =>
      simp [Nat.fib, pow_zero]
    | 1 =>
      simp [Nat.fib, pow_one]
    | n + 2 =>
      rw [Nat.fib_add_two]
      have h_n_simple : Nat.fib n < 2 ^ n := ih n (by simp)
      have h_n_plus_1_simple : Nat.fib (n + 1) < 2 * 2 ^ n := by
        calc
          Nat.fib (n + 1) < 2 ^ (n + 1) := ih (n + 1) (by simp)
          _ = 2 * 2 ^ n                 := by rw [Nat.pow_succ']
      have two_pow_n_plus_2_simple : 2 ^ (n + 2) = 4 * 2 ^ n := by
        calc
          2 ^ (n + 2) = 2 ^ n * 2 ^ 2 := by rw [Nat.pow_add]
          _ = 2 ^ n * 4               := by norm_num
          _ = 4 * 2 ^ n               := by rw [Nat.mul_comm]
      simp only [Nat.fib_add_two, Nat.pow_succ', Nat.pow_add, Nat.pow_two]
      linarith [h_n_simple, h_n_plus_1_simple]

-- Definice Fibonacciho posloupnosti
-- def fib : ℕ → ℕ
--   | 0 => 0
--   | 1 => 1
--   | n + 2 => fib (n + 1) + fib n