The equivalence between ℕ+ and ℕ #
An equivalence between ℕ+ and ℕ given by PNat.natPred and Nat.succPNat.
Equations
- Equiv.pnatEquivNat = { toFun := PNat.natPred, invFun := Nat.succPNat, left_inv := PNat.succPNat_natPred, right_inv := Nat.natPred_succPNat }