Fibonacci cooked 2 ways

Fibonaccis.v

Require Import NArith.

Fixpoint fac_v1 (n : nat) : nat :=
  match n with
  | 0 => 1
  | S n' =>  n * (fac_v1 n')
  end.

Fixpoint visit_fac_v2 (n a : nat) : nat :=
  match n with
  | 0 => a
  | S n' => visit_fac_v2 n' (n * a)
  end.

Definition fac_v2 (n : nat) : nat :=
  visit_fac_v2 n 1.

Require Import ArithRing.

Theorem general_equivalence_of_fac_v1_and_fac_v2 :
  forall n a : nat,
    a * fac_v1 n = visit_fac_v2 n a.
Proof.
intros n; induction n; intro a.
 - simpl ; ring.
 - simpl ; rewrite <- IHn ; ring.
Qed.