import proveit
theory = proveit.Theory() # the theorem's theory
from proveit import x, y, defaults
from proveit.numbers.ordering import min_def_bin
%proving min_x_x_is_x
defaults.assumptions = min_x_x_is_x.conditions
min_def_bin
min_def_bin_inst = min_def_bin.instantiate({x: x, y: x})
The rhs of the min_def_bin_inst above cannot be simplified until we explicitly establish that the second condition is False.
from proveit.numbers.ordering import not_less_from_less_eq
not_less_from_less_eq
not_less_from_less_eq.instantiate({x: x, y: x})
min_def_bin_inst.inner_expr().rhs.simplify()
%qed