@[deprecated Std.not_le (since := "2026-10-09")]

theorem String.not_le {a b : String} : ¬a ≤ b ↔ b < a

@[deprecated Std.not_lt (since := "2026-10-09")]

theorem String.not_lt {a b : String} : ¬a < b ↔ b ≤ a

@[deprecated Std.le_refl (since := "2026-10-09")]

theorem String.le_refl (a : String) : a ≤ a

@[deprecated Std.lt_irrefl (since := "2026-10-09")]

theorem String.lt_irrefl (a : String) : ¬a < a

@[deprecated Std.lt_irrefl (since := "2026-10-09")]

theorem String.le_trans {a b c : String} : a ≤ b → b ≤ c → a ≤ c

@[deprecated Std.lt_irrefl (since := "2026-10-09")]

theorem String.lt_trans {a b c : String} : a < b → b < c → a < c

@[deprecated Std.lt_irrefl (since := "2026-10-09")]

theorem String.le_total (a b : String) : a ≤ b ∨ b ≤ a

@[deprecated Std.lt_irrefl (since := "2026-10-09")]

theorem String.le_antisymm {a b : String} : a ≤ b → b ≤ a → a = b

@[deprecated Std.lt_irrefl (since := "2026-10-09")]

theorem String.lt_asymm {a b : String} (h : a < b) : ¬b < a

@[deprecated Std.lt_irrefl (since := "2026-10-09")]

theorem String.ne_of_lt {a b : String} (h : a < b) : a ≠ b

@[simp]

theorem String.toList_lt_toList_iff {s t : String} : s.toList < t.toList ↔ s < t

@[deprecated String.toList_lt_toList_iff (since := "2026-10-09")]

theorem String.lt_iff {s t : String} : s < t ↔ s.toList < t.toList

@[simp]

theorem String.toList_le_toList_iff {s t : String} : s.toList ≤ t.toList ↔ s ≤ t

@[simp]

theorem String.compare_toList_toList {s t : String} : compare s.toList t.toList = compare s t