Commit 2024-05-05 13:38 1e9f6406
View on Github →refactor(Data/PNat): better OfNat instance (#12420)
Assume [NeZero n] instead of talking about n+1.
This way we can reuse the raw natural literal n in PNat.val_ofNat.
Also add PNat.mk_ofNat and drop some bit0/bit1 lemmas.