Index - P
| plusAssociative | Data.Type.Natural |
| plusCommutative | Data.Type.Natural |
| plusCongL | Data.Type.Natural |
| plusCongR | Data.Type.Natural |
| plusInjectiveL | Data.Type.Natural |
| plusInjectiveR | Data.Type.Natural |
| plusLeqL | Data.Type.Natural |
| plusLeqR | Data.Type.Natural |
| plusMinusEqL | Data.Type.Natural |
| plusMinusEqR | Data.Type.Natural |
| plusMonotone | Data.Type.Natural |
| plusMultDistr | Data.Type.Natural |
| plusNeutralL | Data.Type.Natural |
| plusNeutralR | Data.Type.Natural |
| plusSR | Data.Type.Natural |
| plusZL | Data.Type.Natural |
| plusZR | Data.Type.Natural |
| promote | Data.Type.Natural |
| promoteEqInstance | Data.Type.Natural |
| promoteEqInstances | Data.Type.Natural |
| propToBoolLeq | Data.Type.Natural |
| propToClassLeq | Data.Type.Natural |