Commit 2020-05-19 22:34 3c1f9f9c

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!