theorem String.Slice.skipPrefix?_char_eq_some_iff {c : Char} {s : Slice} {pos : s.Pos} : s.skipPrefix? c = some pos ↔ ∃ (h : s.startPos ≠ s.endPos), pos = s.startPos.next h ∧ s.startPos.get h = c

theorem String.Slice.startsWith_char_iff_get {c : Char} {s : Slice} : s.startsWith c = true ↔ ∃ (h : s.startPos ≠ s.endPos), s.startPos.get h = c

theorem String.Slice.startsWith_char_eq_false_iff_get {c : Char} {s : Slice} : s.startsWith c = false ↔ ∀ (h : s.startPos ≠ s.endPos), s.startPos.get h ≠ c

theorem String.Slice.startsWith_char_eq_head? {c : Char} {s : Slice} : s.startsWith c = (s.copy.toList.head? == some c)

theorem String.Slice.startsWith_char_iff_exists_append {c : Char} {s : Slice} : s.startsWith c = true ↔ ∃ (t : String), s.copy = singleton c ++ t

theorem String.Slice.startsWith_char_eq_false_iff_forall_append {c : Char} {s : Slice} : s.startsWith c = false ↔ ∀ (t : String), s.copy ≠ singleton c ++ t

theorem String.Slice.eq_append_of_dropPrefix?_char_eq_some {c : Char} {s res : Slice} (h : s.dropPrefix? c = some res) : s.copy = singleton c ++ res.copy

theorem String.Slice.skipSuffix?_char_eq_some_iff {c : Char} {s : Slice} {pos : s.Pos} : s.skipSuffix? c = some pos ↔ ∃ (h : s.endPos ≠ s.startPos), pos = s.endPos.prev h ∧ (s.endPos.prev h).get ⋯ = c

theorem String.Slice.endsWith_char_iff_get {c : Char} {s : Slice} : s.endsWith c = true ↔ ∃ (h : s.endPos ≠ s.startPos), (s.endPos.prev h).get ⋯ = c

theorem String.Slice.endsWith_char_eq_false_iff_get {c : Char} {s : Slice} : s.endsWith c = false ↔ ∀ (h : s.endPos ≠ s.startPos), (s.endPos.prev h).get ⋯ ≠ c

theorem String.Slice.endsWith_char_iff_exists_append {c : Char} {s : Slice} : s.endsWith c = true ↔ ∃ (t : String), s.copy = t ++ singleton c

theorem String.Slice.endsWith_char_eq_getLast? {c : Char} {s : Slice} : s.endsWith c = (s.copy.toList.getLast? == some c)

theorem String.Slice.endsWith_char_eq_false_iff_forall_append {c : Char} {s : Slice} : s.endsWith c = false ↔ ∀ (t : String), s.copy ≠ t ++ singleton c

theorem String.Slice.eq_append_of_dropSuffix?_char_eq_some {c : Char} {s res : Slice} (h : s.dropSuffix? c = some res) : s.copy = res.copy ++ singleton c

theorem String.skipPrefix?_char_eq_some_iff {c : Char} {s : String} {pos : s.Pos} : s.skipPrefix? c = some pos ↔ ∃ (h : s.startPos ≠ s.endPos), pos = s.startPos.next h ∧ s.startPos.get h = c

theorem String.startsWith_char_iff_get {c : Char} {s : String} : s.startsWith c = true ↔ ∃ (h : s.startPos ≠ s.endPos), s.startPos.get h = c

theorem String.startsWith_char_eq_false_iff_get {c : Char} {s : String} : s.startsWith c = false ↔ ∀ (h : s.startPos ≠ s.endPos), s.startPos.get h ≠ c

theorem String.startsWith_char_eq_head? {c : Char} {s : String} : s.startsWith c = (s.toList.head? == some c)

theorem String.startsWith_char_iff_exists_append {c : Char} {s : String} : s.startsWith c = true ↔ ∃ (t : String), s = singleton c ++ t

theorem String.startsWith_char_eq_false_iff_forall_append {c : Char} {s : String} : s.startsWith c = false ↔ ∀ (t : String), s ≠ singleton c ++ t

theorem String.eq_append_of_dropPrefix?_char_eq_some {c : Char} {s : String} {res : Slice} (h : s.dropPrefix? c = some res) : s = singleton c ++ res.copy

theorem String.skipSuffix?_char_eq_some_iff {c : Char} {s : String} {pos : s.Pos} : s.skipSuffix? c = some pos ↔ ∃ (h : s.endPos ≠ s.startPos), pos = s.endPos.prev h ∧ (s.endPos.prev h).get ⋯ = c

theorem String.endsWith_char_iff_get {c : Char} {s : String} : s.endsWith c = true ↔ ∃ (h : s.endPos ≠ s.startPos), (s.endPos.prev h).get ⋯ = c

theorem String.endsWith_char_eq_false_iff_get {c : Char} {s : String} : s.endsWith c = false ↔ ∀ (h : s.endPos ≠ s.startPos), (s.endPos.prev h).get ⋯ ≠ c

theorem String.endsWith_char_eq_getLast? {c : Char} {s : String} : s.endsWith c = (s.toList.getLast? == some c)

theorem String.endsWith_char_iff_exists_append {c : Char} {s : String} : s.endsWith c = true ↔ ∃ (t : String), s = t ++ singleton c

theorem String.endsWith_char_eq_false_iff_forall_append {c : Char} {s : String} : s.endsWith c = false ↔ ∀ (t : String), s ≠ t ++ singleton c

theorem String.eq_append_of_dropSuffix?_char_eq_some {c : Char} {s : String} {res : Slice} (h : s.dropSuffix? c = some res) : s = res.copy ++ singleton c