Nat.WithBot.lt_zero_iff

theorem Nat.WithBot.lt_zero_iff : ∀ {n : WithBot ℕ}, n < 0 ↔ n = ⊥

The theorem `Nat.WithBot.lt_zero_iff` states that for any variable `n` of type `WithBot ℕ`, `n` is less than zero if and only if `n` is `⊥` (bottom). In other words, in the context of natural numbers extended with a bottom element (⊥), the only way a number can be considered "less than zero" is if that number is the bottom element itself. This is because natural numbers are non-negative, and the bottom element (`⊥`) is considered less than all natural numbers.

More concisely: In the type of natural numbers extended with a bottom element, a number is less than zero if and only if it is the bottom element itself.