import proveit
from proveit.logic import InSet
from proveit.numbers import Integer
from proveit.physics.quantum.QPE import _best_round_def
from proveit.physics.quantum.QPE import _phase_is_real, _two_pow_t_is_nat_pos
theory = proveit.Theory() # the theorem's theory
%proving _best_round_is_int
_best_round_def
_phase_is_real
_two_pow_t_is_nat_pos
InSet(_best_round_def.rhs, Integer).prove()
%qed