no goals
n : ℕ
⊢ (ack 0 n + 1) ^ 2 ≤ ack (0 + 3) n
simpa using sq_le_two_pow_add_one_minus_three (n + 2)
m : ℕ
⊢ (ack m 1 + 1) ^ 2 ≤ ack (m + 3) 1
m : ℕ
⊢ (ack (m + 1) 0 + 1) ^ 2 ≤ ack (m + 1 + 3) 0
rw [ack_succ_zero, ack_succ_zero]
no goals
m : ℕ
⊢ (ack m 1 + 1) ^ 2 ≤ ack (m + 3) 1
apply ack_add_one_sq_lt_ack_add_three
m n : ℕ
⊢ (ack m (ack (m + 1) n) + 1) ^ 2 ≤ ack (m + 3) (ack (m + 3 + 1) n)
m n : ℕ
⊢ (ack (m + 1) (n + 1) + 1) ^ 2 ≤ ack (m + 1 + 3) (n + 1)
rw [ack_succ_succ, ack_succ_succ]
m n : ℕ
⊢ m + 1 ≤ m + 3 + 1
m n : ℕ
⊢ (ack m (ack (m + 1) n) + 1) ^ 2 ≤ ack (m + 3) (ack (m + 3 + 1) n)
apply (ack_add_one_sq_lt_ack_add_three _ _).trans (ack_mono_right _ <| ack_mono_left _ _)
no goals
m n : ℕ
⊢ m + 1 ≤ m + 3 + 1
linarith