Proof that Fibonacci of n > 0 is less than 2^n

fib.v

(* For the proof idea see https://math.stackexchange.com/a/894767 *)
Require Import Psatz.
From Coq.Arith Require Import PeanoNat.
Import Nat.

Fixpoint fib n :=
  match n with
  | 0 => 1
  | S n =>
    match n with
    | 0 => 1
    | S n' => fib n + fib n'
    end
  end.

Lemma fibPos n: 0 < fib n.
Proof.
  induction n; simpl.
  - lia.
  - destruct n; lia.
Qed.

Lemma fibPow2 : forall n, 0 < n -> fib n < 2 ^ n.
Proof.
  intros n H.
  induction n.
  - inversion H.
  - destruct n as [| [| [| n''']]] eqn:E; try (simpl; lia).
    + replace (2 ^ (S (S (S (S n'''))))) with (2 * 2 ^ (S (S (S n''')))) by (simpl; lia).
      pose proof (IHn ltac:(lia)).
      assert (2 * fib (S (S (S n'''))) < 2 * 2 ^ S (S (S n''')))
        by lia.
      replace (2 * fib (S (S (S n'''))))
        with (fib (S (S (S n'''))) + fib (S (S (S n'''))))
        in H1 by lia.
      replace (fib (S (S (S n'''))))
        with (fib (S (S n''')) + fib (S n'''))
        in H1 at 2 by (unfold fib; lia).
      assert (fib (S (S (S n'''))) + fib (S (S n''')) < fib (S (S (S n'''))) + (fib (S (S n''')) + fib (S n''')))
        by (pose proof (fibPos (S n''')); lia).
      replace (fib (S (S (S n'''))) + fib (S (S n''')))
        with (fib (S (S (S (S n'''))))) in H2 by (unfold fib; lia).
      lia.
Qed.