no goals
n : ℕ
⊢ 0 < ack 0 n
simp
m : ℕ
⊢ 0 < ack m 1
m : ℕ
⊢ 0 < ack (m + 1) 0
rw [ack_succ_zero]
no goals
m : ℕ
⊢ 0 < ack m 1
apply ack_pos
m n : ℕ
⊢ 0 < ack m (ack (m + 1) n)
m n : ℕ
⊢ 0 < ack (m + 1) (n + 1)
rw [ack_succ_succ]
no goals
m n : ℕ
⊢ 0 < ack m (ack (m + 1) n)
apply ack_pos