Package natural-divides-def: Definition of the divides relation on natural numbers
Information
| name | natural-divides-def |
| version | 1.38 |
| description | Definition of the divides relation on natural numbers |
| author | Joe Leslie-Hurd <joe@gilith.com> |
| license | MIT |
| provenance | HOL Light theory extracted on 2012-12-02 |
| requires | bool natural |
| show | Data.Bool Number.Natural |
Files
- Package tarball natural-divides-def-1.38.tgz
- Theory source file natural-divides-def.thy (included in the package tarball)
Defined Constant
- Number
- Natural
- divides
- Natural
Theorem
⊦ ∀a b. divides a b ⇔ ∃c. c * a = b
External Type Operators
- →
- bool
- Number
- Natural
- natural
- Natural
External Constants
- =
- Data
- Bool
- ∀
- ∃
- ⊤
- Bool
- Number
- Natural
- *
- Natural
Assumptions
⊦ ⊤
⊦ (∀) = λp. p = λx. ⊤