Commit 2020-09-14 12:41 e35e287b

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 defs) 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