Axioms for the theory of proveit.numbers.summation

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 a, b, c, f, k, x, fa, fb, fx, alpha
from proveit.core_expr_types import alpha_k
from proveit.logic import Forall, Equals
from proveit.numbers import Add, Exp, Less, LessEq, Mult, number_ordering, subtract, Sum 
from proveit.numbers import one, Interval, Integer

%begin axioms

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

sum_single = Forall(f,
                   Forall(a,
                          Equals(Sum(x, fx, domain=Interval(a,a)), fa),
                          domain=Integer)
                  )

sum_single:

sum_split_last = (
    Forall(f,
           Forall((a, b),
                  Equals(Sum(x, fx, domain=Interval(a, b)),
                         Add(Sum(x, fx, domain=Interval(a, subtract(b, one))), fb)),
                  domain = Integer,
                  conditions = [Less(a, b)])
          ))

sum_split_last:

breakup_sum = Forall(
    (a, b, c),
    Forall((alpha),
    Equals(
    Sum(k, alpha_k, domain=(Interval(a, c))),
    Add(Sum(k, alpha_k, domain=(Interval(a, b))),
        Sum(k, alpha_k, domain=(Interval(Add(b, one), c)))))),
    domain = Integer,
    conditions=[number_ordering(LessEq(a, b), LessEq(b, c))])

breakup_sum:

%end axioms

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