no goals
n₁ n₂ : ℕ
h : n₁ < n₂
⊢ ack 0 n₁ < ack 0 n₂
simpa using h
m n : ℕ
_h : 0 < n + 1
⊢ ack m 1 < ack m (ack (m + 1) n)
m n : ℕ
_h : 0 < n + 1
⊢ ack (m + 1) 0 < ack (m + 1) (n + 1)
rw [ack_succ_zero, ack_succ_succ]
no goals
m n : ℕ
_h : 0 < n + 1
⊢ ack m 1 < ack m (ack (m + 1) n)
exact ack_strictMono_right _ (one_lt_ack_succ_left m n)
m n₁ n₂ : ℕ
h : n₁ + 1 < n₂ + 1
⊢ ack m (ack (m + 1) n₁) < ack m (ack (m + 1) n₂)
m n₁ n₂ : ℕ
h : n₁ + 1 < n₂ + 1
⊢ ack (m + 1) (n₁ + 1) < ack (m + 1) (n₂ + 1)
rw [ack_succ_succ, ack_succ_succ]
m n₁ n₂ : ℕ
h : n₁ + 1 < n₂ + 1
⊢ n₁ < n₂
m n₁ n₂ : ℕ
h : n₁ + 1 < n₂ + 1
⊢ ack m (ack (m + 1) n₁) < ack m (ack (m + 1) n₂)
apply ack_strictMono_right _ (ack_strictMono_right _ _)
no goals
m n₁ n₂ : ℕ
h : n₁ + 1 < n₂ + 1
⊢ n₁ < n₂
rwa [add_lt_add_iff_right] at h