case h.h
m k : ℕ
⊢ hyperoperation 1 m k = m + k
⊢ hyperoperation 1 = fun x x_1 => x + x_1
ext (m k)
case h.h.zero
m : ℕ
⊢ hyperoperation 1 m Nat.zero = m + Nat.zero

case h.h.succ
m bn : ℕ
bih : hyperoperation 1 m bn = m + bn
⊢ hyperoperation 1 m (Nat.succ bn) = m + Nat.succ bn
case h.h
m k : ℕ
⊢ hyperoperation 1 m k = m + k
induction' k with bn bih
no goals
case h.h.zero
m : ℕ
⊢ hyperoperation 1 m Nat.zero = m + Nat.zero
rw [Nat.add_zero m, hyperoperation]
case h.h.succ
m bn : ℕ
bih : hyperoperation 1 m bn = m + bn
⊢ Nat.succ (m + bn) = m + Nat.succ bn
case h.h.succ
m bn : ℕ
bih : hyperoperation 1 m bn = m + bn
⊢ hyperoperation 1 m (Nat.succ bn) = m + Nat.succ bn
rw [hyperoperation_recursion, bih, hyperoperation_zero]
no goals
case h.h.succ
m bn : ℕ
bih : hyperoperation 1 m bn = m + bn
⊢ Nat.succ (m + bn) = m + Nat.succ bn
exact Nat.add_assoc m bn 1