import proveit
theory = proveit.Theory() # the theorem's theory
from proveit import defaults, x
from proveit.numbers.rounding import round_is_an_int
%proving round_of_real_is_real
defaults.assumptions = round_of_real_is_real.conditions
round_is_an_int
round_is_an_int.instantiate({x:x})
%qed