Как мне доказать, что две реализации Фибоначчи равны в Coq?

У меня есть две реализации Фибоначчи, показанные ниже, которые я хочу доказать функционально эквивалентными.

Я уже доказал свойства натуральных чисел, но это упражнение требует другого подхода, который я не могу понять.

Учебник, который я использую, ввел следующий синтаксис Coq, поэтому должна быть возможность доказать равенство с помощью этой записи:

<definition> ::= <keyword> <identifier> : <statement> <proof>

<keyword> ::= Proposition | Lemma | Theorem | Corollary

<statement> ::= {<quantifier>,}* <expression>

<quantifier> ::= forall {<identifier>}+ : <type>
               | forall {({<identifier>}+ : <type>)}+

<proof> ::= Proof. {<tactic>.}* <end-of-proof>

<end-of-proof> ::= Qed. | Admitted. | Abort.

Вот две реализации:

Fixpoint fib_v1 (n : nat) : nat :=
  match n with
  | 0 => O
  | S n' => match n' with
            | O => 1
            | S n'' => (fib_v1 n') + (fib_v1 n'')
            end
  end.

Fixpoint visit_fib_v2 (n a1 a2 : nat) : nat :=
  match n with
  | 0 => a1
  | S n' => visit_fib_v2 n' a2 (a1 + a2)
  end.

Совершенно очевидно, что эти функции вычисляют одно и то же значение для базового случая.n = 0, а вот с индукцией дела обстоят намного сложнее?

Я пытался доказать следующую лемму, но я застрял в индукционном случае:

Lemma about_visit_fib_v2 :
  forall i j : nat,
    visit_fib_v2 i (fib_v1 (S j)) ((fib_v1 j) + (fib_v1 (S j))) = (fib_v1 (add_v1 i (S j))).
Proof.
  induction i as [| i' IHi'].

  intro j.
  rewrite -> (unfold_visit_fib_v2_0 (fib_v1 (S j)) ((fib_v1 j) + (fib_v1 (S j)))).
  rewrite -> (add_v1_0_n (S j)).
  reflexivity.

  intro j.
  rewrite -> (unfold_visit_fib_v2_S i' (fib_v1 (S j)) ((fib_v1 j) + (fib_v1 (S j)))).

 Admitted.

Куда:

Fixpoint add_v1 (i j : nat) : nat :=
  match i with
  | O => j
  | S i' => S (add_v1 i' j)
  end.