feat(data/nat/choose): sum_range_choose_halfway (#2688)
This is a lemma on the way to proving that the product of primes less than `n` is less than `4 ^ n`, which is itself a lemma in Bertrand's postulate.
The lemma itself is of dubious significance, but it will eventually be necessary for Bertrand, and I want to commit early and often. Brief discussion of this decision at https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Candidate.20for.20inclusion.20in.20mathlib/near/197619722 .
This is my second PR to mathlib; the code is definitely verbose and poorly structured, but I don't know how to fix it. I'm expecting almost no lines of the original to remain by the end of this!
Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>
