theorem String.congr_append (a : String) (b : String) : a ++ b = { data := a.data ++ b.data }

@[simp]

theorem String.length_append (as : String) (bs : String) : String.length (as ++ bs) = String.length as + String.length bs

@[simp]

theorem String.length_replicate (n : ℕ) (c : Char) : String.length (String.replicate n c) = n

theorem String.length_eq_list_length (l : List Char) : String.length { data := l } = List.length l

@[simp]

theorem String.leftpad_length (n : ℕ) (c : Char) (s : String) : String.length (String.leftpad n c s) = max n (String.length s)

The length of the String returned by String.leftpad n a c is equal to the larger of n and s.length

theorem String.leftpad_prefix (n : ℕ) (c : Char) (s : String) : String.IsPrefix (String.replicate (n - String.length s) c) (String.leftpad n c s)

theorem String.leftpad_suffix (n : ℕ) (c : Char) (s : String) : String.IsSuffix s (String.leftpad n c s)