abbrev HasInfinity (α : Type) [LT α] := ∃(inf : α), ∀n, n < inf

theorem lt_irrefl_imp_no_infinity
    (α : Type) [LT α] (irrefl : ∀(n : α), ¬n < n) : ¬HasInfinity α := by
  intro h
  have ⟨inf, h⟩ := h
  have hlt : inf < inf := h inf
  exact irrefl inf hlt


theorem no_nat_infinity : ¬HasInfinity Nat :=
  lt_irrefl_imp_no_infinity Nat Nat.lt_irrefl

theorem no_int_infinity : ¬HasInfinity Int :=
  lt_irrefl_imp_no_infinity Int Int.lt_irrefl

-- it's… not difficult to see the pattern