case intro
h : Nat.Primrec fun n => ack n n
m : ℕ
hm : ∀ (n : ℕ), ack n n < ack m n
⊢ False
h : Nat.Primrec fun n => ack n n
⊢ False
cases' exists_lt_ack_of_nat_primrec h with m hm
no goals
case intro
h : Nat.Primrec fun n => ack n n
m : ℕ
hm : ∀ (n : ℕ), ack n n < ack m n
⊢ False
exact (hm m).false