case zero
m : ℕ
⊢ hyperoperation (Nat.zero + 2) m 1 = m

case succ
m nn : ℕ
nih : hyperoperation (nn + 2) m 1 = m
⊢ hyperoperation (Nat.succ nn + 2) m 1 = m
n m : ℕ
⊢ hyperoperation (n + 2) m 1 = m
induction' n with nn nih
case zero
m : ℕ
⊢ (fun x x_1 => x * x_1) m 1 = m
case zero
m : ℕ
⊢ hyperoperation (Nat.zero + 2) m 1 = m
rw [hyperoperation_two]
no goals
case zero
m : ℕ
⊢ (fun x x_1 => x * x_1) m 1 = m
ring
no goals
case succ
m nn : ℕ
nih : hyperoperation (nn + 2) m 1 = m
⊢ hyperoperation (Nat.succ nn + 2) m 1 = m
rw [hyperoperation_recursion, hyperoperation_ge_three_eq_one, nih]