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

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

@[simp]

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

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