import proveit
from proveit import defaults
from proveit import a, b
from proveit.logic import InSet
from proveit.numbers import Add, Integer
from proveit.numbers.modular import mod_int_closure
from proveit.physics.quantum.QPE import _two_pow_t # common
from proveit.physics.quantum.QPE import _mod_add_def # axioms
from proveit.physics.quantum.QPE import _two_pow_t_is_nat_pos # theorems
theory = proveit.Theory() # the theorem's theory
%proving _mod_add_closure
defaults.assumptions = _mod_add_closure.conditions
_mod_add_def
mod_add_def_inst = _mod_add_def.instantiate({a:a, b:b})
mod_add_def_inst.rhs.deduce_in_interval()
%qed