mathlib3

e35e287b - refactor(data/nat/*): cleanup data.nat.basic, split data.nat.choose (#4135)

refactor(data/nat/*): cleanup data.nat.basic, split data.nat.choose (#4135) This PR rearranges `data.nat.basic` so the lemmas are now in (hopefully appropriately-named) markdown sections. It also moves several sections (mostly ones that introduced new `def`s) into new files: - `data.nat.fact` - `data.nat.psub` (maybe this could be named `data.nat.partial`?) - `data.nat.log` - `data.nat.with_bot` `data.nat.choose` has been split into a directory: - The definition of `nat.choose` and basic lemmas about it have been moved from `data.nat.basic` into `data.nat.choose.basic` - The binomial theorem and related lemmas involving sums are now in `data.nat.choose.sum`; the following lemmas are now in the `nat` namespace: - `sum_range_choose` - `sum_range_choose_halfway` - `choose_middle_le_pow` - Divisibility properties of binomial coefficients are now in `data.nat.choose.dvd`. Other changes: - added `nat.pow_two_sub_pow_two` to `data.nat.basic`. - module docs & doc strings for `data.nat.sqrt` Co-authored-by: Rob Lewis <Rob.y.lewis@gmail.com>