theorem String.data_eq_of_eq {a b : String} (h : a = b) : a.data = b.data

theorem String.ne_of_data_ne {a b : String} (h : a.data ≠ b.data) : a ≠ b

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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

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

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

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