AccT

inductive AccT {α : Type u} (r : α → α → Sort v) : α → Type (max u v) where
  | intro (x : α) (h : (y : α) → r y x → AccT r y) : AccT r x

namespace AccT

def inv {x y : α} : (h₁ : AccT r x) → (h₂ : r y x) → AccT r y
| ⟨_, h⟩, h₂ => h y h₂

def NatAccT : (n : Nat) → @AccT Nat (. < .) n
| 0 => AccT.intro 0 (fun y h => (Nat.not_lt_zero y h).elim)
| (n+1) => AccT.intro (n+1)
  (fun m h =>
    if hmn : m = n
      then hmn ▸ NatAccT n
      else
        have hmln : m < n := Nat.lt_of_le_of_ne (Nat.le_of_lt_succ h) hmn
        inv (NatAccT n) hmln)


noncomputable def fib (n : Nat) : Nat :=
AccT.recOn (NatAccT n) fun n _ =>
  match n with
  | 0 => fun _ => 1
  | 1 => fun _ => 1
  | (n+2) => fun ih =>
    ih n (Nat.lt_trans (Nat.lt_succ_self _) (Nat.lt_succ_self _)) + 
      ih (n+1) (Nat.lt_succ_self _)

example (n : Nat) : fib (n + 2) = fib n + fib (n+1) := by
rw [fib]
dsimp [NatAccT]