Documentation
Init
.
GrindInstances
.
Nat
Search
return to top
source
Imports
Init.Omega
Init.Grind.Ordered.Module
Imported by
Lean
.
Grind
.
instAddRightCancelNat
Lean
.
Grind
.
instExistsAddOfLTNat
← Mathematical handbook
source
instance
Lean
.
Grind
.
instAddRightCancelNat
:
AddRightCancel
Nat
source
instance
Lean
.
Grind
.
instExistsAddOfLTNat
:
ExistsAddOfLT
Nat