Coqりさん 証明のかけら

Coq りさん Coq りさん、フィボナッチ数列の末尾再帰にしたやつって、本当に元のと同じなんですか？

Fixpoint fib1 (n : nat) : nat :=
 match n with
  | 0 => 0
  | 1 => 1
  | S n => fib1 n + fib1 (pred n)
 end.

Fixpoint fib2 (a b n : nat) : nat :=
 match n with
  | 0 => a
  | S n => fib2 b (a + b) n
 end.

Theorem fib_eq : forall (n:nat), fib1 n = fib2 0 1 n.
Proof.
  intro n.
  induction n.
    simpl.
    reflexivity.
    
    (*´・ω・｀*)
Qed.