Axioms for the theory of proveit.numbers.absolute_value

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
from proveit.logic import Equals, Forall
from proveit.numbers import two, Abs, Exp, Real, sqrt

%begin axioms

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

# this axiom might be shifted to theorems once we have
# the Conditional class to use for a piece-wise definition
abs_val_def_sqrt = Forall(
    x,
    Equals(Abs(x), sqrt(Exp(x, two))),
    domain = Real)

abs_val_def_sqrt:

%end axioms

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