(* I renamed this from factorial to factorial_rec. *)
Fixpoint factorial_rec (n: nat): nat :=
  match n with
  | O => 1
  | S n' => n * factorial_rec n'
  end.

Eval compute in (factorial_rec 5).

Inductive factorial : nat -> nat -> Prop :=
  | fact_base : factorial O 1
  | fact_step : forall n m, factorial n m -> factorial (S n) ((S n) * m).

Example factorial_5 : factorial 5 120.
Proof.
  apply (fact_step 4 24).
  apply (fact_step 3 6).
  apply (fact_step 2 2).
  apply (fact_step 1 1).
  apply (fact_step O 1). (* The step ChatGPT missed. *)
  apply fact_base.
Qed.

Lemma factorial_equiv : forall n, factorial n (factorial_rec n).
Proof.
  induction n.
  - apply fact_base.
  - simpl.
    apply (fact_step n (factorial_rec n)).
    apply IHn.
Qed.

(* This generated lemma was incorrect. I rewrote the claim manually and generated a new proof. *)
(* Lemma factorial_rec_equiv : forall n, factorial_rec n = factorial n. *)
(* Proof. *)
  (* intros n. *)
  (* unfold factorial_rec. *)
  (* induction n. *)
  (* - reflexivity. *)
  (* - simpl. *)
    (* rewrite IHn. *)
    (* apply (fact_step n (factorial n)). *)
    (* apply factorial_equiv. *)
(* Qed. *)

Lemma factorial_rec_equiv : forall n m, factorial_rec n = m -> factorial n m.
Proof.
  intros n m H.
  rewrite <- H.
  clear H.
  induction n.
  - apply fact_base.
  - simpl.
    apply (fact_step n (factorial_rec n)).
    apply IHn.
    (* reflexivity. *) (* This proved (ha) unnecessary. *)
Qed.