mathlib

9363a649 - feat(data/nat/choose/sum): Add lower bound lemma for central binomial coefficient (#7214)

feat(data/nat/choose/sum): Add lower bound lemma for central binomial coefficient (#7214) This lemma complements the one above it, and will be useful in proving Bertrand's postulate from the 100 theorems list.