Commit 2026-04-29 14:11 6cf3ab1c

View on Github →

chore: make argument in zero_le/one_le implicit (#38148) This matches bot_le and is quite more convenient in practice. Among the hundreds of times we use this theorem, we require the explicit argument only 8 (or 13, counting tactics).

Estimated changes

modified theorem kstar_zero
modified theorem eq_one_or_one_lt
modified theorem isBot_one
added theorem ne_one_of_lt
modified theorem not_lt_one
modified theorem one_le
modified theorem ENat.one_le_epow
modified theorem Finsupp.le_iff'
modified theorem Dynamics.coverMincard_empty
modified theorem Ordinal.zero_div