| Leq | Data.Type.Natural |
| leqAntisymm | Data.Type.Natural.Class.Order, Data.Type.Natural.Class, Data.Type.Natural |
| LeqInstance | Data.Type.Natural |
| leqNeqToLT | Data.Type.Natural.Class.Order, Data.Type.Natural.Class, Data.Type.Natural |
| leqNeqToSuccLeq | Data.Type.Natural.Class.Order, Data.Type.Natural.Class, Data.Type.Natural |
| leqqAndLeq | Data.Type.Natural.Builtin |
| leqRefl | Data.Type.Natural.Class.Order, Data.Type.Natural.Class, Data.Type.Natural |
| leqReflexive | Data.Type.Natural.Class.Order, Data.Type.Natural.Class, Data.Type.Natural |
| leqReversed | Data.Type.Natural.Class.Order, Data.Type.Natural.Class, Data.Type.Natural |
| leqStep | Data.Type.Natural.Class.Order, Data.Type.Natural.Class, Data.Type.Natural |
| LeqSucc | Data.Type.Natural.Class.Order, Data.Type.Natural.Class |
| leqSucc | Data.Type.Natural.Class.Order, Data.Type.Natural.Class, Data.Type.Natural |
| leqSucc' | Data.Type.Natural.Class.Order, Data.Type.Natural.Class, Data.Type.Natural |
| leqSuccStepL | Data.Type.Natural.Class.Order, Data.Type.Natural.Class, Data.Type.Natural |
| leqSuccStepR | Data.Type.Natural.Class.Order, Data.Type.Natural.Class, Data.Type.Natural |
| leqToCmp | Data.Type.Natural.Class.Order, Data.Type.Natural.Class, Data.Type.Natural |
| leqToGT | Data.Type.Natural.Class.Order, Data.Type.Natural.Class, Data.Type.Natural |
| leqToLT | Data.Type.Natural.Class.Order, Data.Type.Natural.Class, Data.Type.Natural |
| leqToMax | Data.Type.Natural.Class.Order, Data.Type.Natural.Class, Data.Type.Natural |
| leqToMin | Data.Type.Natural.Class.Order, Data.Type.Natural.Class, Data.Type.Natural |
| leqTrans | Data.Type.Natural.Class.Order, Data.Type.Natural.Class, Data.Type.Natural |
| LeqView | Data.Type.Natural.Class.Order, Data.Type.Natural.Class |
| leqViewRefl | Data.Type.Natural.Class.Order, Data.Type.Natural.Class, Data.Type.Natural |
| leqWitness | Data.Type.Natural.Class.Order, Data.Type.Natural.Class, Data.Type.Natural |
| LeqZero | Data.Type.Natural.Class.Order, Data.Type.Natural.Class |
| leqZero | Data.Type.Natural.Class.Order, Data.Type.Natural.Class, Data.Type.Natural |
| leqZeroElim | Data.Type.Natural.Class.Order, Data.Type.Natural.Class, Data.Type.Natural |
| lneqReversed | Data.Type.Natural.Class.Order, Data.Type.Natural.Class, Data.Type.Natural |
| lneqRightPredSucc | Data.Type.Natural.Class.Order, Data.Type.Natural.Class, Data.Type.Natural |
| lneqSucc | Data.Type.Natural.Class.Order, Data.Type.Natural.Class, Data.Type.Natural |
| lneqSuccLeq | Data.Type.Natural.Class.Order, Data.Type.Natural.Class, Data.Type.Natural |
| lneqSuccStepL | Data.Type.Natural.Class.Order, Data.Type.Natural.Class, Data.Type.Natural |
| lneqSuccStepR | Data.Type.Natural.Class.Order, Data.Type.Natural.Class, Data.Type.Natural |
| lneqToLT | Data.Type.Natural.Class.Order, Data.Type.Natural.Class, Data.Type.Natural |
| lneqZero | Data.Type.Natural.Class.Order, Data.Type.Natural.Class, Data.Type.Natural |
| lneqZeroAbsurd | Data.Type.Natural.Class.Order, Data.Type.Natural.Class, Data.Type.Natural |
| ltRightPredSucc | Data.Type.Natural.Class.Order, Data.Type.Natural.Class, Data.Type.Natural |
| ltSucc | Data.Type.Natural.Class.Order, Data.Type.Natural.Class, Data.Type.Natural |
| ltSuccLToLT | Data.Type.Natural.Class.Order, Data.Type.Natural.Class, Data.Type.Natural |
| LTSym0 | Data.Type.Natural.Class.Order, Data.Type.Natural.Class, Data.Type.Natural.Builtin |
| ltToLeq | Data.Type.Natural.Class.Order, Data.Type.Natural.Class, Data.Type.Natural |
| ltToLneq | Data.Type.Natural.Class.Order, Data.Type.Natural.Class, Data.Type.Natural |
| ltToNeq | Data.Type.Natural.Class.Order, Data.Type.Natural.Class, Data.Type.Natural |
| ltToSuccLeq | Data.Type.Natural.Class.Order, Data.Type.Natural.Class, Data.Type.Natural |