Commit 2025-11-04 18:11 8a851dd1

View on Github →

feat(Data/PNat/Basic): add order-related instances to PNat (#26453) Add SuccAddOrder ℕ+ and NoMaxOrder ℕ+ instances.

Estimated changes

added theorem PNat.succ_eq_add_one