Commit 2026-03-20 06:03 b65c1329

View on Github →

chore: robustify ENat/Basic (#36885) Failing on experimental lean-pr-testing-NNNN branches, so let's make it more robust.

Estimated changes

added theorem ENat.succ_coe
added theorem ENat.succ_top