Commit 2025-09-21 21:36 24d97c4b

View on Github →

chore(Data/Nat/Choose): add le-version of a bound and fix name of the lt-version (#29821)

Estimated changes

modified theorem Nat.choose_le_two_pow
added theorem Nat.choose_lt_two_pow