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