feat: Add String.length_join and List.length_join

[tjf801]

Quick fix for #770.

[tjf801]

awaiting-review

[digama0]

This is a cross cutting import, and also not a precise import. The needed theorem(s) should move to Std.Data.Nat.Init.Lemmas and that should be imported here. If you only need the definition then it can just be an import of Std.Data.Nat.Basic.

[kim-em]

Is it possible to move the needed lemmas up into an Init folder, to reduce the imports needed here?

[urkud]

Note that Mathlib has https://leanprover-community.github.io/mathlib4_docs/Mathlib/Algebra/BigOperators/List/Basic.html#List.length_join stated in terms of a generic List.sum instead of Nat.sum. What's the migration plan?

[kim-em]

Given that mathlib already has a List.length_join, we'll need to have a PR for mathlib that uses this branch of Std ready to go before this can be merged.