theorem Nat.eq_of_not_lt_not_lt {a b : Nat} : ¬a < b → ¬b < a → a = b