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