Commit 2022-12-21 16:29 3f6e3098

View on Github →

feat: port data.nat.choose.bounds (#1139) Port of data.nat.choose.bounds based on 550b58538991c8977703fdeb7c9d51a5aa27df11

Estimated changes

added theorem Nat.choose_le_pow
added theorem Nat.pow_le_choose