Axioms for the theory of proveit.numbers.divisibility

import proveit
# Prepare this notebook for defining the axioms of a theory:
%axioms_notebook # Keep this at the top following 'import proveit'.
from proveit import x, y
from proveit.logic import Equals, Exists, Forall, InSet
from proveit.numbers import Integer
from proveit.numbers import Divides, frac

%begin axioms

Defining axioms for theory 'proveit.numbers.divisibility'
Subsequent end-of-cell assignments will define axioms
%end_axioms will finalize the definitions

divides_def = Forall(
        (x, y),
        Equals(Divides(x, y), InSet(frac(y, x), Integer)))

divides_def:

%end axioms

These axioms may now be imported from the theory package: proveit.numbers.divisibility