Theorem PNat.succ_eq_add_one

Modification history

2025-11-04 18:11

Mathlib/Data/PNat/Order.lean

feat(Data/PNat/Basic): add order-related instances to PNat (#26453) …

Added PNat.succ_eq_add_one View on Github →