Package natural-divides-def: Definition of the divides relation on natural numbers

Information

namenatural-divides-def
version1.37
descriptionDefinition of the divides relation on natural numbers
authorJoe Leslie-Hurd <joe@gilith.com>
licenseMIT
provenanceHOL Light theory extracted on 2012-11-10
requiresbool
natural
showData.Bool
Number.Natural

Files

Defined Constant

Theorem

a b. divides a b c. c * a = b

Input Type Operators

Input Constants

Assumptions

() = λp. p = λx.