no goals
n : ℕ
⊢ 1 < ack 0 (n + 1)
simp
m n : ℕ
⊢ 1 < ack m (ack (m + 1) n)
m n : ℕ
⊢ 1 < ack (m + 1) (n + 1)
rw [ack_succ_succ]
case intro
m n h✝ : ℕ
h : ack (m + 1) n = succ h✝
⊢ 1 < ack m (ack (m + 1) n)
m n : ℕ
⊢ 1 < ack m (ack (m + 1) n)
cases' exists_eq_succ_of_ne_zero (ack_pos (m + 1) n).ne' with h h
case intro
m n h✝ : ℕ
h : ack (m + 1) n = succ h✝
⊢ 1 < ack m (succ h✝)
case intro
m n h✝ : ℕ
h : ack (m + 1) n = succ h✝
⊢ 1 < ack m (ack (m + 1) n)
rw [h]
no goals
case intro
m n h✝ : ℕ
h : ack (m + 1) n = succ h✝
⊢ 1 < ack m (succ h✝)
apply one_lt_ack_succ_right