no goals
m : ℕ
_h : 0 < m + 1
⊢ ack 0 0 < ack (m + 1) 0
simpa using one_lt_ack_succ_right m 0
m n : ℕ
h : 0 < m + 1
⊢ n + 1 + 1 < ack m (ack (m + 1) n)
m n : ℕ
h : 0 < m + 1
⊢ ack 0 (n + 1) < ack (m + 1) (n + 1)
rw [ack_zero, ack_succ_succ]
m n : ℕ
h : 0 < m + 1
⊢ n + 1 + 1 ≤ m + (m + 1 + n + 1)
m n : ℕ
h : 0 < m + 1
⊢ n + 1 + 1 < ack m (ack (m + 1) n)
apply lt_of_le_of_lt (le_trans _ <| add_le_add_left (add_add_one_le_ack _ _) m) (add_lt_ack _ _)
no goals
m n : ℕ
h : 0 < m + 1
⊢ n + 1 + 1 ≤ m + (m + 1 + n + 1)
linarith
no goals
m₁ m₂ : ℕ
h : m₁ + 1 < m₂ + 1
⊢ ack (m₁ + 1) 0 < ack (m₂ + 1) 0
simpa using ack_strict_mono_left' 1 ((add_lt_add_iff_right 1).1 h)
m₁ m₂ n : ℕ
h : m₁ + 1 < m₂ + 1
⊢ ack m₁ (ack (m₁ + 1) n) < ack m₂ (ack (m₂ + 1) n)
m₁ m₂ n : ℕ
h : m₁ + 1 < m₂ + 1
⊢ ack (m₁ + 1) (n + 1) < ack (m₂ + 1) (n + 1)
rw [ack_succ_succ, ack_succ_succ]
no goals
m₁ m₂ n : ℕ
h : m₁ + 1 < m₂ + 1
⊢ ack m₁ (ack (m₁ + 1) n) < ack m₂ (ack (m₂ + 1) n)
exact
  (ack_strict_mono_left' _ <| (add_lt_add_iff_right 1).1 h).trans
    (ack_strictMono_right _ <| ack_strict_mono_left' n h)