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

@[simp]

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

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

@[simp]

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

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.replicate (n - s.length) c).IsPrefix (String.leftpad n c s)

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