String.length_append

Stream: batteries

[tjf801]

Should there be a similar lemma to List.length_append with the rest of the String lemmas? It's a pretty short proof too, so I'm not really sure why it's not in there already, for convenience's sake

@[simp] theorem length_append (s1 s2 : String) : (s1 ++ s2).length = s1.length + s2.length := by
  simp only [String.length, String.append, List.length_append]

[Mario Carneiro]

sure, PRs welcome